🐜 Small fixes

Project.toml

@@ -2,7 +2,7 @@ name = "Pluto"
 uuid = "c3e4b0f8-55cb-11ea-2926-15256bba5781"
 license = "MIT"
 authors = ["Fons van der Plas <[email protected]>", "Mikołaj Bochenski <[email protected]>"]
-version = "0.4.1"
+version = "0.4.2"
 
 [deps]
 HTTP = "cd3eb016-35fb-5094-929b-558a96fad6f3"

assets/client.js

@@ -8,7 +8,6 @@ class PlutoConnection {
             },
             redirect: 'follow',
             referrerPolicy: 'no-referrer',
-            //body: "hiiiii"
         }).then((response) => {
             return response.json()
         }).then((response) => {
@@ -21,14 +20,16 @@ class PlutoConnection {
     }
 
     waitForOnline() {
+        this.currentlyConnected = false
         this.onDisconnect()
 
         setTimeout(() => {
             this.ping(() => {
                 if (this.psocket.readyState != WebSocket.OPEN) {
                     this.waitForOnline()
                 } else {
-                    this.onConnect()
+                    this.currentlyConnected = true
+                    this.onReconnect()
                 }
             }, () => {
                 this.waitForOnline()
@@ -111,6 +112,7 @@ class PlutoConnection {
         this.psocket.onopen = () => {
             this.send("connect", {})
             this.send("getallnotebooks", {})
+            this.currentlyConnected = true
             console.log("socket opened")
             onSucces()
         }
@@ -126,14 +128,23 @@ class PlutoConnection {
             this.startSocketConnection(() => {
                 this.onEstablishConnection()
             })
-        }, this.onDisconnect)
+        }, () => {
+            this.currentlyConnected = true
+            this.onDisconnect()
+        })
     }
 
-    constructor(onUpdate, onEstablishConnection, onConnect, onDisconnect){
+    constructor(onUpdate, onEstablishConnection, onReconnect, onDisconnect){
         this.onUpdate = onUpdate
         this.onEstablishConnection = onEstablishConnection
-        this.onConnect = onConnect
+        this.onReconnect = onReconnect
         this.onDisconnect = onDisconnect
+
+        this.currentlyConnected = false
+
+        window.addEventListener("unload", e => {
+            this.send("disconnect", {})
+        })
     }
 
     // TODO: reconnect with a delay if the last request went poorly

assets/editor.html

@@ -80,9 +80,9 @@
         } */
 
         main {
-            min-height: calc(100vh - 100px - 4em);
             margin: 0 auto;
             margin-top: 100px;
+            min-height: calc(100vh - 100px - 4em);
             max-width: 960px;
             align-content: center;
             padding: 8px;
@@ -96,7 +96,7 @@
             z-index: 20;
             background: hsla(0, 100%, 100%, 80%);
             width: 100%;
-            min-height: 70px;
+            min-height: 60px;
             overflow: hidden;
             /* white-space: nowrap; */
             /*font-weight: normal;*/
@@ -112,7 +112,7 @@
         #logocontainer {
             margin: 0 auto;
             max-width: 960px;
-            padding-top: 13px;
+            padding-top: 10px;
             padding-left: 20px;
             padding-bottom: 0px;
         }
@@ -134,7 +134,7 @@
             display: inline;
             border-bottom: none;
             font-family: 'Roboto Mono', monospace !important;
-            font-size: 1.1em;
+            font-size: 0.8em;
             letter-spacing: 1px;
         }
 
@@ -145,7 +145,7 @@
         #printernametitle {
             opacity: .6;
             font-style: normal;
-            font-weight: 400;
+            font-weight: 500;
         }
 
         body.disconnected>header {

assets/editor.js

@@ -363,17 +363,27 @@ document.addEventListener("DOMContentLoaded", () => {
         }, 3000)
     }
 
-    function onConnect() {
+    function onReconnect() {
         document.body.classList.remove("disconnected")
         document.querySelector("meta[name=theme-color]").content = "#fff"
+        for (var uuid in window.codeMirrors) {
+            window.codeMirrors[uuid].options.disableInput = false
+        }
     }
 
     function onDisconnect() {
         document.body.classList.add("disconnected")
         document.querySelector("meta[name=theme-color]").content = "#DEAF91"
+        setTimeout(() => {
+            if(!client.currentlyConnected){
+                for (var uuid in window.codeMirrors) {
+                    window.codeMirrors[uuid].options.disableInput = true
+                }
+            }
+        }, 5000)
     }
 
-    window.client = new PlutoConnection(onUpdate, onEstablishConnection, onConnect, onDisconnect)
+    window.client = new PlutoConnection(onUpdate, onEstablishConnection, onReconnect, onDisconnect)
     client.notebookID = notebookID
     client.initialize()
 

src/react/WorkspaceManager.jl

@@ -52,7 +52,6 @@ function get_workspace(notebook::Notebook)::Workspace
 end
 
 function delete_funcs(notebook::Notebook, to_delete::Set{Symbol})
-    # TODO: treat methods separately
     ws = get_workspace(notebook)
     for funcname in to_delete
         try
@@ -69,7 +68,6 @@ function delete_funcs(notebook::Notebook, to_delete::Set{Symbol})
 end
 
 function delete_vars(notebook::Notebook, to_delete::Set{Symbol})
-    # TODO: treat methods separately
     ws = get_workspace(notebook)
     ws.deleted_vars = ws.deleted_vars ∪ to_delete
 end

src/webserver/Dynamic.jl

@@ -1,5 +1,9 @@
 import JSON
 
+# JSON.jl doesn't define a serialization method for MIME objects, so we add one ourselves:
+import JSON: lower
+JSON.lower(m::MIME) = string(m)
+
 struct UpdateMessage
     type::Symbol
     message::Any

src/webserver/NotebookServer.jl

@@ -99,7 +99,9 @@ responses = Dict{Symbol,Function}()
 addresponse(f::Function, endpoint::Symbol) = responses[endpoint] = f
 
 
-"Will _synchronously_ run the notebook server. (i.e. blocking call)"
+"""Start a Pluto server _synchronously_ (i.e. blocking call) on `http://localhost:[port]/`.
+
+This will start the static HTTP server and a WebSocket server. Pluto Notebooks will be started dynamically (by user input)."""
 function run(port = 1234, launchbrowser = false)
     serversocket = Sockets.listen(UInt16(port))
     @async HTTP.serve(Sockets.localhost, UInt16(port), stream = true, server = serversocket) do http::HTTP.Stream
@@ -131,6 +133,7 @@ function run(port = 1234, launchbrowser = false)
 
                             if messagetype == :disconnect
                                 delete!(connectedclients, client.id)
+                                close(clientstream)
                             elseif messagetype == :connect
                                 # nothing more to do
                             else