diff --git a/demo/package-lock.json b/demo/package-lock.json
index bef6ff8..5d7d39e 100644
--- a/demo/package-lock.json
+++ b/demo/package-lock.json
@@ -30,7 +30,7 @@
       }
     },
     "..": {
-      "version": "1.0.29",
+      "version": "1.0.30",
       "license": "Apache-2.0",
       "dependencies": {
         "@leanprover/infoview": "^0.7.3",
diff --git a/demo/src/LeanMonaco.tsx b/demo/src/LeanMonaco.tsx
index b1f90c9..ecb084d 100644
--- a/demo/src/LeanMonaco.tsx
+++ b/demo/src/LeanMonaco.tsx
@@ -10,16 +10,18 @@ function LeanMonacoComponent({options, numberEditors} : {options: LeanMonacoOpti
 
   // You need to start one `LeanMonaco` instance once in your application using a `useEffect`
   useEffect(() => {
-    const leanMonaco = new LeanMonaco()
-    setLeanMonaco(leanMonaco)
-    leanMonaco.setInfoviewElement(infoviewRef.current!)
+    var _leanMonaco = new LeanMonaco()
+    setLeanMonaco(_leanMonaco)
+    _leanMonaco.setInfoviewElement(infoviewRef.current!)
+
 
     ;(async () => {
-      await leanMonaco.start(options)
+      await _leanMonaco.start(options)
+      console.debug('[demo]: leanMonaco started')
     })()
 
     return () => {
-      leanMonaco.dispose()
+      _leanMonaco.dispose()
     }
   }, [options])
 
@@ -34,7 +36,7 @@ function LeanMonacoComponent({options, numberEditors} : {options: LeanMonacoOpti
 
       <div>
         <button onClick={(ev)=> {
-          console.log('restarting Lean')
+          console.log('[LeanMonaco] restarting Lean')
           leanMonaco?.clientProvider?.getClients().map(client => {client.restart()})
         }}>Restart Lean</button>
       </div>
diff --git a/demo/src/LeanMonacoEditor.tsx b/demo/src/LeanMonacoEditor.tsx
index b21161c..13f1b01 100644
--- a/demo/src/LeanMonacoEditor.tsx
+++ b/demo/src/LeanMonacoEditor.tsx
@@ -13,7 +13,9 @@ function LeanMonacoEditorComponent({fileName, value}: {fileName: string, value:
 
       ;(async () => {
         await leanMonaco!.whenReady
+        console.debug('[demo]: starting editor')
         await leanMonacoEditor.start(codeviewRef.current!, fileName, value)
+        console.debug('[demo]: editor started')
       })()
 
       return () => {
diff --git a/package-lock.json b/package-lock.json
index 1885203..8d6e905 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -34,9 +34,9 @@
       }
     },
     "node_modules/@babel/runtime": {
-      "version": "7.25.0",
-      "resolved": "https://registry.npmjs.org/@babel/runtime/-/runtime-7.25.0.tgz",
-      "integrity": "sha512-7dRy4DwXwtzBrPbZflqxnvfxLF8kdZXPkhymtDeFoFqE6ldzjQFgYTtYIFARcLEYDrqfBfYcZt1WqFxRoyC9Rw==",
+      "version": "7.25.4",
+      "resolved": "https://registry.npmjs.org/@babel/runtime/-/runtime-7.25.4.tgz",
+      "integrity": "sha512-DSgLeL/FNcpXuzav5wfYvHCGvynXkJbn3Zvc3823AEe9nPwW9IK4UoCSS5yGymmQzN0pCPvivtgS6/8U2kkm1w==",
       "dependencies": {
         "regenerator-runtime": "^0.14.0"
       },
@@ -583,26 +583,6 @@
         "cypress": "*"
       }
     },
-    "node_modules/@types/eslint": {
-      "version": "9.6.0",
-      "resolved": "https://registry.npmjs.org/@types/eslint/-/eslint-9.6.0.tgz",
-      "integrity": "sha512-gi6WQJ7cHRgZxtkQEoyHMppPjq9Kxo5Tjn2prSKDSmZrCz8TZ3jSRCeTJm+WoM+oB0WG37bRqLzaaU3q7JypGg==",
-      "dev": true,
-      "dependencies": {
-        "@types/estree": "*",
-        "@types/json-schema": "*"
-      }
-    },
-    "node_modules/@types/eslint-scope": {
-      "version": "3.7.7",
-      "resolved": "https://registry.npmjs.org/@types/eslint-scope/-/eslint-scope-3.7.7.tgz",
-      "integrity": "sha512-MzMFlSLBqNF2gcHWO0G1vP/YQyfvrxZ0bF+u7mzUdZ1/xK4A4sru+nraZz5i3iEIk1l1uyicaDVTB4QbbEkAYg==",
-      "dev": true,
-      "dependencies": {
-        "@types/eslint": "*",
-        "@types/estree": "*"
-      }
-    },
     "node_modules/@types/estree": {
       "version": "1.0.5",
       "resolved": "https://registry.npmjs.org/@types/estree/-/estree-1.0.5.tgz",
@@ -616,9 +596,9 @@
       "dev": true
     },
     "node_modules/@types/node": {
-      "version": "22.4.1",
-      "resolved": "https://registry.npmjs.org/@types/node/-/node-22.4.1.tgz",
-      "integrity": "sha512-1tbpb9325+gPnKK0dMm+/LMriX0vKxf6RnB0SZUqfyVkQ4fMgUSySqhxE/y8Jvs4NyF1yHzTfG9KlnkIODxPKg==",
+      "version": "22.5.0",
+      "resolved": "https://registry.npmjs.org/@types/node/-/node-22.5.0.tgz",
+      "integrity": "sha512-DkFrJOe+rfdHTqqMg0bSNlGlQ85hSoh2TPzZyhHsXnMtligRWpxUySiyw8FY14ITt24HVCiQPWxS3KO/QlGmWg==",
       "dev": true,
       "dependencies": {
         "undici-types": "~6.19.2"
@@ -1738,9 +1718,9 @@
       }
     },
     "node_modules/dayjs": {
-      "version": "1.11.12",
-      "resolved": "https://registry.npmjs.org/dayjs/-/dayjs-1.11.12.tgz",
-      "integrity": "sha512-Rt2g+nTbLlDWZTwwrIXjy9MeiZmSDI375FvZs72ngxx8PDC6YXOeR3q5LAuPzjZQxhiWdRKac7RKV+YyQYfYIg==",
+      "version": "1.11.13",
+      "resolved": "https://registry.npmjs.org/dayjs/-/dayjs-1.11.13.tgz",
+      "integrity": "sha512-oaMBel6gjolK862uaPQOVTA7q3TZhuSvuMQAAglQDOWYO9A91IrAOUJEyKVlqJlHE0vq5p5UXxzdPfMH/x6xNg==",
       "dev": true
     },
     "node_modules/debug": {
@@ -1797,9 +1777,9 @@
       }
     },
     "node_modules/electron-to-chromium": {
-      "version": "1.5.12",
-      "resolved": "https://registry.npmjs.org/electron-to-chromium/-/electron-to-chromium-1.5.12.tgz",
-      "integrity": "sha512-tIhPkdlEoCL1Y+PToq3zRNehUaKp3wBX/sr7aclAWdIWjvqAe/Im/H0SiCM4c1Q8BLPHCdoJTol+ZblflydehA==",
+      "version": "1.5.13",
+      "resolved": "https://registry.npmjs.org/electron-to-chromium/-/electron-to-chromium-1.5.13.tgz",
+      "integrity": "sha512-lbBcvtIJ4J6sS4tb5TLp1b4LyfCdMkwStzXPyAgVgTRAsep4bvrAGaBOP7ZJtQMNJpSQ9SqG4brWOroNaQtm7Q==",
       "dev": true
     },
     "node_modules/emoji-regex": {
@@ -2544,9 +2524,9 @@
       }
     },
     "node_modules/is-core-module": {
-      "version": "2.15.0",
-      "resolved": "https://registry.npmjs.org/is-core-module/-/is-core-module-2.15.0.tgz",
-      "integrity": "sha512-Dd+Lb2/zvk9SKy1TGCt1wFJFo/MWBPMX5x7KcvLajWTGuomczdQX61PvY5yK6SVACwpoexWo81IfFyoKY2QnTA==",
+      "version": "2.15.1",
+      "resolved": "https://registry.npmjs.org/is-core-module/-/is-core-module-2.15.1.tgz",
+      "integrity": "sha512-z0vtXSwucUJtANQWldhbtbt7BnL0vxiFjIdDLAatwhDYty2bad6s+rijD6Ri4YuYJubLzIJLUidCh09e1djEVQ==",
       "dev": true,
       "dependencies": {
         "hasown": "^2.0.2"
@@ -3063,40 +3043,40 @@
       }
     },
     "node_modules/monaco-editor-wrapper": {
-      "version": "5.5.1",
-      "resolved": "https://registry.npmjs.org/monaco-editor-wrapper/-/monaco-editor-wrapper-5.5.1.tgz",
-      "integrity": "sha512-Urgzu7J1Yd1j3K7+hm2P5vvW45Ryq7Q21RN6f7TyEeC2aKnw080UpiY5G/fOWzjH+OGXdulNp0ut4CQUX1/v2A==",
-      "dependencies": {
-        "@codingame/monaco-vscode-configuration-service-override": "~8.0.1",
-        "@codingame/monaco-vscode-editor-service-override": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-cs": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-de": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-es": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-fr": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-it": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-ja": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-ko": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-pl": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-pt-br": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-qps-ploc": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-ru": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-tr": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-zh-hans": "~8.0.1",
-        "@codingame/monaco-vscode-language-pack-zh-hant": "~8.0.1",
-        "@codingame/monaco-vscode-monarch-service-override": "~8.0.1",
-        "@codingame/monaco-vscode-textmate-service-override": "~8.0.1",
-        "@codingame/monaco-vscode-theme-defaults-default-extension": "~8.0.1",
-        "@codingame/monaco-vscode-theme-service-override": "~8.0.1",
-        "monaco-editor": "npm:@codingame/monaco-vscode-editor-api@~8.0.1",
-        "vscode": "npm:@codingame/monaco-vscode-api@~8.0.1",
+      "version": "5.5.2",
+      "resolved": "https://registry.npmjs.org/monaco-editor-wrapper/-/monaco-editor-wrapper-5.5.2.tgz",
+      "integrity": "sha512-YuoIV2hxqGpgYGFshsDNvItLMKeriCbFcroCo/NinrEDzr2PlWuIFbaKBr2r6to2sNq53d6iUpjz6P7PTe/nrw==",
+      "dependencies": {
+        "@codingame/monaco-vscode-configuration-service-override": "~8.0.2",
+        "@codingame/monaco-vscode-editor-service-override": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-cs": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-de": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-es": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-fr": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-it": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-ja": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-ko": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-pl": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-pt-br": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-qps-ploc": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-ru": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-tr": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-zh-hans": "~8.0.2",
+        "@codingame/monaco-vscode-language-pack-zh-hant": "~8.0.2",
+        "@codingame/monaco-vscode-monarch-service-override": "~8.0.2",
+        "@codingame/monaco-vscode-textmate-service-override": "~8.0.2",
+        "@codingame/monaco-vscode-theme-defaults-default-extension": "~8.0.2",
+        "@codingame/monaco-vscode-theme-service-override": "~8.0.2",
+        "monaco-editor": "npm:@codingame/monaco-vscode-editor-api@~8.0.2",
+        "vscode": "npm:@codingame/monaco-vscode-api@~8.0.2",
         "vscode-languageclient": "~9.0.1",
         "vscode-languageserver-protocol": "~3.17.5",
         "vscode-ws-jsonrpc": "~3.3.2"
       },
       "peerDependencies": {
-        "monaco-editor": "npm:@codingame/monaco-vscode-editor-api@~8.0.1",
-        "monaco-languageclient": "~8.8.1",
-        "vscode": "npm:@codingame/monaco-vscode-api@~8.0.1"
+        "monaco-editor": "npm:@codingame/monaco-vscode-editor-api@~8.0.2",
+        "monaco-languageclient": "~8.8.2",
+        "vscode": "npm:@codingame/monaco-vscode-api@~8.0.2"
       },
       "peerDependenciesMeta": {
         "monaco-editor": {
@@ -3111,17 +3091,17 @@
       }
     },
     "node_modules/monaco-languageclient": {
-      "version": "8.8.1",
-      "resolved": "https://registry.npmjs.org/monaco-languageclient/-/monaco-languageclient-8.8.1.tgz",
-      "integrity": "sha512-fgI4tFfsZRSB7igkN6vossoprZet3kydCGxh2OtEZNECvkpXBhXi55V4/UyyevhDS3Hwrh8O7ApfzoVX5uJyXg==",
+      "version": "8.8.2",
+      "resolved": "https://registry.npmjs.org/monaco-languageclient/-/monaco-languageclient-8.8.2.tgz",
+      "integrity": "sha512-qE5LaHcTELjGMbq3iwBq1DqBEjzEYsPHaQUeAqNmGAFyMEJ0O+wldXAQgAqfB+oWrh2xmSiFcizmXqRawrx8oQ==",
       "peer": true,
       "dependencies": {
-        "@codingame/monaco-vscode-extensions-service-override": "~8.0.1",
-        "@codingame/monaco-vscode-languages-service-override": "~8.0.1",
-        "@codingame/monaco-vscode-localization-service-override": "~8.0.1",
-        "@codingame/monaco-vscode-model-service-override": "~8.0.1",
-        "monaco-editor": "npm:@codingame/monaco-vscode-editor-api@~8.0.1",
-        "vscode": "npm:@codingame/monaco-vscode-api@~8.0.1",
+        "@codingame/monaco-vscode-extensions-service-override": "~8.0.2",
+        "@codingame/monaco-vscode-languages-service-override": "~8.0.2",
+        "@codingame/monaco-vscode-localization-service-override": "~8.0.2",
+        "@codingame/monaco-vscode-model-service-override": "~8.0.2",
+        "monaco-editor": "npm:@codingame/monaco-vscode-editor-api@~8.0.2",
+        "vscode": "npm:@codingame/monaco-vscode-api@~8.0.2",
         "vscode-languageclient": "~9.0.1"
       },
       "engines": {
@@ -3129,8 +3109,8 @@
         "npm": ">=9.0.0"
       },
       "peerDependencies": {
-        "monaco-editor": "npm:@codingame/monaco-vscode-editor-api@~8.0.1",
-        "vscode": "npm:@codingame/monaco-vscode-api@~8.0.1"
+        "monaco-editor": "npm:@codingame/monaco-vscode-editor-api@~8.0.2",
+        "vscode": "npm:@codingame/monaco-vscode-api@~8.0.2"
       },
       "peerDependenciesMeta": {
         "monaco-editor": {
@@ -4493,12 +4473,11 @@
       }
     },
     "node_modules/webpack": {
-      "version": "5.93.0",
-      "resolved": "https://registry.npmjs.org/webpack/-/webpack-5.93.0.tgz",
-      "integrity": "sha512-Y0m5oEY1LRuwly578VqluorkXbvXKh7U3rLoQCEO04M97ScRr44afGVkI0FQFsXzysk5OgFAxjZAb9rsGQVihA==",
+      "version": "5.94.0",
+      "resolved": "https://registry.npmjs.org/webpack/-/webpack-5.94.0.tgz",
+      "integrity": "sha512-KcsGn50VT+06JH/iunZJedYGUJS5FGjow8wb9c0v5n1Om8O1g4L6LjtfxwlXIATopoQu+vOXXa7gYisWxCoPyg==",
       "dev": true,
       "dependencies": {
-        "@types/eslint-scope": "^3.7.3",
         "@types/estree": "^1.0.5",
         "@webassemblyjs/ast": "^1.12.1",
         "@webassemblyjs/wasm-edit": "^1.12.1",
@@ -4507,7 +4486,7 @@
         "acorn-import-attributes": "^1.9.5",
         "browserslist": "^4.21.10",
         "chrome-trace-event": "^1.0.2",
-        "enhanced-resolve": "^5.17.0",
+        "enhanced-resolve": "^5.17.1",
         "es-module-lexer": "^1.2.1",
         "eslint-scope": "5.1.1",
         "events": "^3.2.0",
diff --git a/src/leanmonaco.ts b/src/leanmonaco.ts
index 235ac75..b4ba2a0 100644
--- a/src/leanmonaco.ts
+++ b/src/leanmonaco.ts
@@ -62,20 +62,27 @@ export type LeanMonacoOptions = {
     console.debug('[LeanMonaco]: starting')
 
     if (LeanMonaco.activeInstance == this) {
-      console.warn('A LeanMonaco instance cannot be started twice.')
+      console.warn('[LeanMonaco]: A LeanMonaco instance cannot be started twice.')
       return
     }
     if (LeanMonaco.activeInstance) {
-      console.warn('There can only be one active LeanMonaco instance at a time. Disposing previous instance.')
+      console.warn('[LeanMonaco]: There can only be one active LeanMonaco instance at a time. Disposing previous instance.')
       LeanMonaco.activeInstance?.dispose()
     }
     LeanMonaco.activeInstance = this
 
     if (! window.MonacoEnvironment) {
+      console.debug('[LeanMonaco]: setting monaco environment')
       type WorkerLoader = () => Worker
       const workerLoaders: Partial<Record<string, WorkerLoader>> = {
-        editorWorkerService: () => new Worker(new URL('monaco-editor/esm/vs/editor/editor.worker.js', import.meta.url), { type: 'module' }),
-        textMateWorker: () => new Worker(new URL('@codingame/monaco-vscode-textmate-service-override/worker', import.meta.url), { type: 'module' }),
+        editorWorkerService: () => new Worker(
+          new URL('monaco-editor/esm/vs/editor/editor.worker.js', import.meta.url),
+          { type: 'module' }
+        ),
+        textMateWorker: () => new Worker(
+          new URL('@codingame/monaco-vscode-textmate-service-override/worker', import.meta.url),
+          { type: 'module' }
+        ),
       }
       window.MonacoEnvironment = {
         getWorker: function (moduleId, label) {
@@ -102,19 +109,22 @@ export type LeanMonacoOptions = {
           workspaceProvider: {
             trusted: true,
             workspace: {
-                workspaceUri: Uri.file('/workspace.code-workspace')
+              workspaceUri: Uri.file('/workspace.code-workspace')
             },
             async open() {
-                return false
+              return false
             }
           }
         }
       )
-
+      console.debug('[LeanMonaco]: done initializing')
     }
     await (await import('@codingame/monaco-vscode-theme-defaults-default-extension')).whenReady
 
-    if (this.disposed) return
+    if (this.disposed) {
+      console.debug('[LeanMonaco]: is disposed (A)')
+      return
+    }
 
     this.extensionRegisterResult = registerExtension(this.getExtensionManifest(), ExtensionHostKind.LocalProcess)
 
@@ -125,12 +135,18 @@ export type LeanMonacoOptions = {
 
     await this.extensionRegisterResult.whenReady()
 
-    if (this.disposed) return
+    if (this.disposed) {
+      console.debug('[LeanMonaco]: is disposed (B)')
+      return
+    }
 
     const themeService = await getService(IThemeService)
     const configurationService = await getService(IConfigurationService)
 
-    if (this.disposed) return
+    if (this.disposed) {
+      console.debug('[LeanMonaco]: is disposed (C)')
+      return
+    }
 
     this.updateVSCodeOptions(options.vscode ?? {})
 
@@ -206,8 +222,12 @@ export type LeanMonacoOptions = {
       ...options.vscode
     })
 
-    if (this.disposed) return
+    if (this.disposed) {
+      console.debug('[LeanMonaco]: is disposed (D)')
+      return
+    }
 
+    console.info('[LeanMonaco]: is ready!')
     this.ready()
   }
 
diff --git a/src/vscode-lean4 b/src/vscode-lean4
index 9b38cf3..0b3cbc2 160000
--- a/src/vscode-lean4
+++ b/src/vscode-lean4
@@ -1 +1 @@
-Subproject commit 9b38cf30b5f1c4c4fdc24ffe0366c60199790643
+Subproject commit 0b3cbc2a3f4a005cab8ada8888b4f1577a2064ba
diff --git a/tsconfig.json b/tsconfig.json
index c28b877..f1b02dc 100644
--- a/tsconfig.json
+++ b/tsconfig.json
@@ -3,7 +3,7 @@
     "target": "ESNext",
     "useDefineForClassFields": true,
     "module": "ESNext",
-    "lib": ["ES2020", "DOM", "DOM.Iterable"],
+    "lib": ["ES2021", "ES2021.String", "DOM", "DOM.Iterable"],
     "skipLibCheck": true,
 
     /* Bundler mode */