fixes

client/src/App.tsx

@@ -52,11 +52,6 @@ function App() {
   const [url, setUrl] = useState<string | null>(null)
   const [codeFromUrl, setCodeFromUrl] = useState<string>('')
 
-  /** Restart the Lean client. */
-  function restart() {
-    leanMonaco?.clientProvider?.getClients().map(client => {client.restart()})
-  }
-
   /** Monaco editor requires the code to be set manually. */
   function setContent (code: string) {
     editor?.getModel()?.setValue(code)
@@ -118,7 +113,7 @@ function App() {
   // Update LeanMonaco options when preferences are loaded or change
   useEffect(() => {
     var socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") +
-      window.location.host + "/websocket" + "/" + project
+      window.location.host + "/websocket/" + project
     console.log(`[Lean4web] socket url: ${socketUrl}`)
     var _options: LeanMonacoOptions = {
       websocket: {url: socketUrl},
@@ -155,7 +150,7 @@ function App() {
     _leanMonaco.setInfoviewElement(infoviewRef.current!)
     ;(async () => {
         await _leanMonaco.start(options)
-        await leanMonacoEditor.start(editorRef.current!, `/project/${project}.lean`, '')
+        await leanMonacoEditor.start(editorRef.current!, `/project/${project}.lean`, code)
 
         setEditor(leanMonacoEditor.editor)
         setLeanMonaco(_leanMonaco)
@@ -360,7 +355,7 @@ function App() {
           setProject={setProject}
           setUrl={setUrl}
           codeFromUrl={codeFromUrl}
-          restart={restart}
+          restart={leanMonaco?.restart}
           codeMirror={codeMirror}
           setCodeMirror={setCodeMirror}
           />

client/src/Navigation.tsx

@@ -141,7 +141,7 @@ export const Menu: FC <{
   setProject: Dispatch<SetStateAction<string>>,
   setUrl: Dispatch<SetStateAction<string | null>>,
   codeFromUrl: string,
-  restart: () => void,
+  restart?: () => void,
   codeMirror: boolean,
   setCodeMirror: Dispatch<SetStateAction<boolean>>,
 }> = ({code, setContent, project, setProject, setUrl, codeFromUrl, restart, codeMirror, setCodeMirror}) => {

server/index.mjs

@@ -77,12 +77,12 @@ function startServerProcess(project) {
   let projectPath = __dirname + `/../Projects/` + project
 
   let serverProcess
-  if (!isDevelopment) {
-    console.info("Running with Bubblewrap container.")
-    serverProcess = cp.spawn("./bubblewrap.sh", [projectPath], { cwd: __dirname })
-  } else {
+  if (isDevelopment) {
     console.warn("Running without Bubblewrap container!")
     serverProcess = cp.spawn("lean", ["--server"], { cwd: projectPath })
+  } else {
+    console.info("Running with Bubblewrap container.")
+    serverProcess = cp.spawn("./bubblewrap.sh", [projectPath], { cwd: __dirname })
   }
 
   // serverProcess.stdout.on('data', (data) => {
@@ -98,7 +98,7 @@ function startServerProcess(project) {
   )
 
   serverProcess.on('close', (code) => {
-    console.log(`child process exited with code ${code}`);
+    console.log(`lean server exited with code ${code}`);
   });
 
   return serverProcess
@@ -124,12 +124,16 @@ wss.addListener("connection", function(ws, req) {
   const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
   const serverConnection = jsonrpcserver.createProcessStreamConnection(ps)
   socketConnection.forward(serverConnection, message => {
-      // console.log(`CLIENT: ${JSON.stringify(message)}`)
-      return message;
+    // if (isDevelopment) {
+    //   console.log(`CLIENT: ${JSON.stringify(message)}`)
+    // }
+    return message;
   })
   serverConnection.forward(socketConnection, message => {
-      // console.log(`SERVER: ${JSON.stringify(message)}`)
-      return message;
+    // if (isDevelopment) {
+    //   console.log(`SERVER: ${JSON.stringify(message)}`)
+    // }
+    return message;
   });
 
   ws.on('close', () => {

vite.config.ts

@@ -14,7 +14,8 @@ export default defineConfig({
     esbuildOptions: {
       // @ts-ignore           // TODO
       plugins: [importMetaUrlPlugin]
-    }
+    },
+    exclude: ['Projects']
   },
   build: {
     // Relative to the root