diff --git a/client/public/onigasm.wasm b/client/public/onigasm.wasm
new file mode 100644
index 0000000..3915937
Binary files /dev/null and b/client/public/onigasm.wasm differ
diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 7f43d34..911ccb6 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -12,6 +12,7 @@ import InputZone from './InputZone';
 import Message from './Message';
 import TacticState from './TacticState';
 import * as rpc from 'vscode-ws-jsonrpc';
+import Editor from 'lean4web/client/src/Editor'
 
 interface LevelProps {
   rpcConnection: null|rpc.MessageConnection;
@@ -103,8 +104,10 @@ function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, set
         <LeftPanel spells={tacticDocs} inventory={lemmaDocs} />
       </Grid>
       <Grid xs={4}>
-        <InputZone index={index} history={history} messageOpen={messageOpen} setMessageOpen={setMessageOpen} completed={completed} sendTactic={sendTactic} nbLevels={nbLevels} loadNextLevel={loadNextLevel}
-          errors={errors} lastTactic={lastTactic} undo={undo} finishGame={finishGame} />
+        <Editor setRestart={() => {}}
+          value={""} onDidChangeContent={() => {}}/>
+        {/* <InputZone index={index} history={history} messageOpen={messageOpen} setMessageOpen={setMessageOpen} completed={completed} sendTactic={sendTactic} nbLevels={nbLevels} loadNextLevel={loadNextLevel}
+          errors={errors} lastTactic={lastTactic} undo={undo} finishGame={finishGame} /> */}
         <Message isOpen={messageOpen} content={message} close={closeMessage} />
       </Grid>
       <Grid xs={4}>
diff --git a/package-lock.json b/package-lock.json
index 6483b13..2764345 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -14,6 +14,8 @@
         "@mui/material": "^5.10.9",
         "better-react-mathjax": "^2.0.2",
         "express": "^4.18.2",
+        "lean4web": "git+https://github.com/hhu-adam/lean4web.git",
+        "path-browserify": "^1.0.1",
         "react": "^18.2.0",
         "react-dom": "^18.2.0",
         "react-markdown": "^8.0.3",
@@ -1540,6 +1542,17 @@
       "resolved": "https://registry.npmjs.org/@emotion/weak-memoize/-/weak-memoize-0.3.0.tgz",
       "integrity": "sha512-AHPmaAx+RYfZz0eYu6Gviiagpmiyw98ySSlQvCUhVGDRtDFe4DBS0x1bSjdF3gqUDYOczB+yYvBTtEylYSdRhg=="
     },
+    "node_modules/@esm-bundle/react": {
+      "version": "17.0.2-fix.1",
+      "resolved": "https://registry.npmjs.org/@esm-bundle/react/-/react-17.0.2-fix.1.tgz",
+      "integrity": "sha512-AzHd8Hi5KQjwgU2e3SD1XrMm5WF8y8zsKmP9ttsyR6bzTS8TAc1mWRc8UW0Q/px4D38mcP4+ofJDAhhFiB7KXg==",
+      "hasInstallScript": true
+    },
+    "node_modules/@esm-bundle/react-dom": {
+      "version": "17.0.2-fix.0",
+      "resolved": "https://registry.npmjs.org/@esm-bundle/react-dom/-/react-dom-17.0.2-fix.0.tgz",
+      "integrity": "sha512-U0ofefDbwOtgBh3kOAXklRoYDN9COtjVFiQ8aW7/H8FmBi96S8PYtm4xObITSqjDfvZOWC4Z1g1p3zsgBr8PGw=="
+    },
     "node_modules/@fontsource/roboto": {
       "version": "4.5.8",
       "resolved": "https://registry.npmjs.org/@fontsource/roboto/-/roboto-4.5.8.tgz",
@@ -1550,6 +1563,51 @@
       "resolved": "https://registry.npmjs.org/@fontsource/roboto-mono/-/roboto-mono-4.5.8.tgz",
       "integrity": "sha512-AW44UkbQD0w1CT5mzDbsvhGZ6/bb0YmZzoELj6Sx8vcVEzcbYGUdt2Dtl5zqlOuYMWQFY1mniwWyVv+Bm/lVxw=="
     },
+    "node_modules/@fortawesome/fontawesome-common-types": {
+      "version": "6.2.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.2.1.tgz",
+      "integrity": "sha512-Sz07mnQrTekFWLz5BMjOzHl/+NooTdW8F8kDQxjWwbpOJcnoSg4vUDng8d/WR1wOxM0O+CY9Zw0nR054riNYtQ==",
+      "hasInstallScript": true,
+      "engines": {
+        "node": ">=6"
+      }
+    },
+    "node_modules/@fortawesome/fontawesome-svg-core": {
+      "version": "6.2.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.2.1.tgz",
+      "integrity": "sha512-HELwwbCz6C1XEcjzyT1Jugmz2NNklMrSPjZOWMlc+ZsHIVk+XOvOXLGGQtFBwSyqfJDNgRq4xBCwWOaZ/d9DEA==",
+      "hasInstallScript": true,
+      "dependencies": {
+        "@fortawesome/fontawesome-common-types": "6.2.1"
+      },
+      "engines": {
+        "node": ">=6"
+      }
+    },
+    "node_modules/@fortawesome/free-solid-svg-icons": {
+      "version": "6.2.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.2.1.tgz",
+      "integrity": "sha512-oKuqrP5jbfEPJWTij4sM+/RvgX+RMFwx3QZCZcK9PrBDgxC35zuc7AOFsyMjMd/PIFPeB2JxyqDr5zs/DZFPPw==",
+      "hasInstallScript": true,
+      "dependencies": {
+        "@fortawesome/fontawesome-common-types": "6.2.1"
+      },
+      "engines": {
+        "node": ">=6"
+      }
+    },
+    "node_modules/@fortawesome/react-fontawesome": {
+      "version": "0.2.0",
+      "resolved": "https://registry.npmjs.org/@fortawesome/react-fontawesome/-/react-fontawesome-0.2.0.tgz",
+      "integrity": "sha512-uHg75Rb/XORTtVt7OS9WoK8uM276Ufi7gCzshVWkUJbHhh3svsUUeqXerrM96Wm7fRiDzfKRwSoahhMIkGAYHw==",
+      "dependencies": {
+        "prop-types": "^15.8.1"
+      },
+      "peerDependencies": {
+        "@fortawesome/fontawesome-svg-core": "~1 || ~6",
+        "react": ">=16.3"
+      }
+    },
     "node_modules/@jridgewell/gen-mapping": {
       "version": "0.3.2",
       "resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.2.tgz",
@@ -1608,6 +1666,24 @@
         "@jridgewell/sourcemap-codec": "1.4.14"
       }
     },
+    "node_modules/@leanprover/infoview": {
+      "version": "0.2.0",
+      "resolved": "git+ssh://git@github.com/abentkamp/infoview-npm.git#eb2e3982eded7f7f45fe245a5b20c4804fb82079",
+      "license": "Apache-2.0",
+      "dependencies": {
+        "@leanprover/infoview-api": "^0.1.0",
+        "@vscode/codicons": "0.0.28",
+        "marked": "^4.0.17",
+        "react-fast-compare": "^3.2.0",
+        "tachyons": "^4.12.0",
+        "vscode-languageserver-protocol": "^3.17.2"
+      }
+    },
+    "node_modules/@leanprover/infoview-api": {
+      "version": "0.1.0",
+      "resolved": "https://registry.npmjs.org/@leanprover/infoview-api/-/infoview-api-0.1.0.tgz",
+      "integrity": "sha512-vNMFrk5U1UlWhHp7G1e33mG7hJHyIErb3INgsVITbEW8CzOlAUrc83Pp3ARZykIc8++WJhT7WH+lALo8nO7G0Q=="
+    },
     "node_modules/@leichtgewicht/ip-codec": {
       "version": "2.0.4",
       "resolved": "https://registry.npmjs.org/@leichtgewicht/ip-codec/-/ip-codec-2.0.4.tgz",
@@ -2298,6 +2374,11 @@
         "@types/node": "*"
       }
     },
+    "node_modules/@vscode/codicons": {
+      "version": "0.0.28",
+      "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.28.tgz",
+      "integrity": "sha512-p8zph8Tflh6KUirDCVOti8tr/BhngQx9Z6QXSKBJgPTZMxiKmP6eF75AKDopUeffp7X80Vdo48nv4kdW9d73Dg=="
+    },
     "node_modules/@webassemblyjs/ast": {
       "version": "1.11.1",
       "resolved": "https://registry.npmjs.org/@webassemblyjs/ast/-/ast-1.11.1.tgz",
@@ -2655,6 +2736,14 @@
       "resolved": "https://registry.npmjs.org/array-flatten/-/array-flatten-1.1.1.tgz",
       "integrity": "sha512-PCVAQswWemu6UdxsDFFX/+gVeYqKAod3D3UVm91jHwynguOwAvYPhx8nNlM++NqRcK6CxxpUafjmhIdKiHibqg=="
     },
+    "node_modules/axios": {
+      "version": "0.24.0",
+      "resolved": "https://registry.npmjs.org/axios/-/axios-0.24.0.tgz",
+      "integrity": "sha512-Q6cWsys88HoPgAaFAVUb0WpPk0O8iTeisR9IMqy9G8AbO4NlpVknrnQS03zzF9PGAWgO3cgletO3VjV/P7VztA==",
+      "dependencies": {
+        "follow-redirects": "^1.14.4"
+      }
+    },
     "node_modules/babel-loader": {
       "version": "8.2.5",
       "resolved": "https://registry.npmjs.org/babel-loader/-/babel-loader-8.2.5.tgz",
@@ -2729,8 +2818,7 @@
     "node_modules/balanced-match": {
       "version": "1.0.2",
       "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.2.tgz",
-      "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw==",
-      "dev": true
+      "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw=="
     },
     "node_modules/batch": {
       "version": "0.6.1",
@@ -2821,11 +2909,15 @@
       "integrity": "sha512-hNfzcOV8W4NdualtqBFPyVO+54DSJuZGY9qT4pRroB6S9e3iiido2ISIC5h9R2sPJ8H3FHCIiEnsv1lPXO3KtQ==",
       "dev": true
     },
+    "node_modules/boolbase": {
+      "version": "1.0.0",
+      "resolved": "https://registry.npmjs.org/boolbase/-/boolbase-1.0.0.tgz",
+      "integrity": "sha512-JZOSA7Mo9sNGB8+UjSgzdLtokWAky1zbztM3WRLCbZ70/3cTANmQmOdR7y2g+J0e2WXywy1yS468tY+IruqEww=="
+    },
     "node_modules/brace-expansion": {
       "version": "1.1.11",
       "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.11.tgz",
       "integrity": "sha512-iCuPHDFgrHX7H2vEI/5xpz07zSHB00TpugqhmYtVmMO6518mCuRMoOYFldEBl0g187ufozdaHgWKcYFb61qGiA==",
-      "dev": true,
       "dependencies": {
         "balanced-match": "^1.0.0",
         "concat-map": "0.0.1"
@@ -2877,6 +2969,11 @@
       "integrity": "sha512-E+XQCRwSbaaiChtv6k6Dwgc+bx+Bs6vuKJHHl5kox/BaKbhiXzqQOwK4cO22yElGp2OCmjwVhT3HmxgyPGnJfQ==",
       "dev": true
     },
+    "node_modules/builtin-status-codes": {
+      "version": "3.0.0",
+      "resolved": "https://registry.npmjs.org/builtin-status-codes/-/builtin-status-codes-3.0.0.tgz",
+      "integrity": "sha512-HpGFw18DgFWlncDfjTa2rcQ4W88O1mC8e8yZ2AvQY5KDaktSTwo+KRf6nHK6FRI5FyRyb/5T6+TSxfP7QyGsmQ=="
+    },
     "node_modules/bytes": {
       "version": "3.1.2",
       "resolved": "https://registry.npmjs.org/bytes/-/bytes-3.1.2.tgz",
@@ -2955,6 +3052,42 @@
         "url": "https://github.com/sponsors/wooorm"
       }
     },
+    "node_modules/cheerio": {
+      "version": "1.0.0-rc.12",
+      "resolved": "https://registry.npmjs.org/cheerio/-/cheerio-1.0.0-rc.12.tgz",
+      "integrity": "sha512-VqR8m68vM46BNnuZ5NtnGBKIE/DfN0cRIzg9n40EIq9NOv90ayxLBXA8fXC5gquFRGJSTRqBq25Jt2ECLR431Q==",
+      "dependencies": {
+        "cheerio-select": "^2.1.0",
+        "dom-serializer": "^2.0.0",
+        "domhandler": "^5.0.3",
+        "domutils": "^3.0.1",
+        "htmlparser2": "^8.0.1",
+        "parse5": "^7.0.0",
+        "parse5-htmlparser2-tree-adapter": "^7.0.0"
+      },
+      "engines": {
+        "node": ">= 6"
+      },
+      "funding": {
+        "url": "https://github.com/cheeriojs/cheerio?sponsor=1"
+      }
+    },
+    "node_modules/cheerio-select": {
+      "version": "2.1.0",
+      "resolved": "https://registry.npmjs.org/cheerio-select/-/cheerio-select-2.1.0.tgz",
+      "integrity": "sha512-9v9kG0LvzrlcungtnJtpGNxY+fzECQKhK4EGJX2vByejiMX84MFNQw4UxPJl3bFbTMw+Dfs37XaIkCwTZfLh4g==",
+      "dependencies": {
+        "boolbase": "^1.0.0",
+        "css-select": "^5.1.0",
+        "css-what": "^6.1.0",
+        "domelementtype": "^2.3.0",
+        "domhandler": "^5.0.3",
+        "domutils": "^3.0.1"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/fb55"
+      }
+    },
     "node_modules/chokidar": {
       "version": "3.5.3",
       "resolved": "https://registry.npmjs.org/chokidar/-/chokidar-3.5.3.tgz",
@@ -3124,8 +3257,7 @@
     "node_modules/concat-map": {
       "version": "0.0.1",
       "resolved": "https://registry.npmjs.org/concat-map/-/concat-map-0.0.1.tgz",
-      "integrity": "sha512-/Srv4dswyQNBfohGpz9o6Yb3Gz3SrUDqBH5rTuhGR7ahtlbYKnVxw2bCFMRljaA7EXHaXZ8wsHdodFvbkhKmqg==",
-      "dev": true
+      "integrity": "sha512-/Srv4dswyQNBfohGpz9o6Yb3Gz3SrUDqBH5rTuhGR7ahtlbYKnVxw2bCFMRljaA7EXHaXZ8wsHdodFvbkhKmqg=="
     },
     "node_modules/concurrently": {
       "version": "7.4.0",
@@ -3474,6 +3606,32 @@
         "node": ">=10"
       }
     },
+    "node_modules/css-select": {
+      "version": "5.1.0",
+      "resolved": "https://registry.npmjs.org/css-select/-/css-select-5.1.0.tgz",
+      "integrity": "sha512-nwoRF1rvRRnnCqqY7updORDsuqKzqYJ28+oSMaJMMgOauh3fvwHqMS7EZpIPqK8GL+g9mKxF1vP/ZjSeNjEVHg==",
+      "dependencies": {
+        "boolbase": "^1.0.0",
+        "css-what": "^6.1.0",
+        "domhandler": "^5.0.2",
+        "domutils": "^3.0.1",
+        "nth-check": "^2.0.1"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/fb55"
+      }
+    },
+    "node_modules/css-what": {
+      "version": "6.1.0",
+      "resolved": "https://registry.npmjs.org/css-what/-/css-what-6.1.0.tgz",
+      "integrity": "sha512-HTUrgRJ7r4dsZKU6GjmpfRK1O76h97Z8MfS1G0FozR+oF2kG6Vfe8JE6zwrkbxigziPHinCJ+gCPjA9EaBDtRw==",
+      "engines": {
+        "node": ">= 6"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/fb55"
+      }
+    },
     "node_modules/cssesc": {
       "version": "3.0.0",
       "resolved": "https://registry.npmjs.org/cssesc/-/cssesc-3.0.0.tgz",
@@ -3641,6 +3799,57 @@
         "csstype": "^3.0.2"
       }
     },
+    "node_modules/dom-serializer": {
+      "version": "2.0.0",
+      "resolved": "https://registry.npmjs.org/dom-serializer/-/dom-serializer-2.0.0.tgz",
+      "integrity": "sha512-wIkAryiqt/nV5EQKqQpo3SToSOV9J0DnbJqwK7Wv/Trc92zIAYZ4FlMu+JPFW1DfGFt81ZTCGgDEabffXeLyJg==",
+      "dependencies": {
+        "domelementtype": "^2.3.0",
+        "domhandler": "^5.0.2",
+        "entities": "^4.2.0"
+      },
+      "funding": {
+        "url": "https://github.com/cheeriojs/dom-serializer?sponsor=1"
+      }
+    },
+    "node_modules/domelementtype": {
+      "version": "2.3.0",
+      "resolved": "https://registry.npmjs.org/domelementtype/-/domelementtype-2.3.0.tgz",
+      "integrity": "sha512-OLETBj6w0OsagBwdXnPdN0cnMfF9opN69co+7ZrbfPGrdpPVNBUj02spi6B1N7wChLQiPn4CSH/zJvXw56gmHw==",
+      "funding": [
+        {
+          "type": "github",
+          "url": "https://github.com/sponsors/fb55"
+        }
+      ]
+    },
+    "node_modules/domhandler": {
+      "version": "5.0.3",
+      "resolved": "https://registry.npmjs.org/domhandler/-/domhandler-5.0.3.tgz",
+      "integrity": "sha512-cgwlv/1iFQiFnU96XXgROh8xTeetsnJiDsTc7TYCLFd9+/WNkIqPTxiM/8pSd8VIrhXGTf1Ny1q1hquVqDJB5w==",
+      "dependencies": {
+        "domelementtype": "^2.3.0"
+      },
+      "engines": {
+        "node": ">= 4"
+      },
+      "funding": {
+        "url": "https://github.com/fb55/domhandler?sponsor=1"
+      }
+    },
+    "node_modules/domutils": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/domutils/-/domutils-3.0.1.tgz",
+      "integrity": "sha512-z08c1l761iKhDFtfXO04C7kTdPBLi41zwOZl00WS8b5eiaebNpY00HKbztwBq+e3vyqWNwWF3mP9YLUeqIrF+Q==",
+      "dependencies": {
+        "dom-serializer": "^2.0.0",
+        "domelementtype": "^2.3.0",
+        "domhandler": "^5.0.1"
+      },
+      "funding": {
+        "url": "https://github.com/fb55/domutils?sponsor=1"
+      }
+    },
     "node_modules/ee-first": {
       "version": "1.1.1",
       "resolved": "https://registry.npmjs.org/ee-first/-/ee-first-1.1.1.tgz",
@@ -3688,6 +3897,17 @@
         "node": ">=10.13.0"
       }
     },
+    "node_modules/entities": {
+      "version": "4.4.0",
+      "resolved": "https://registry.npmjs.org/entities/-/entities-4.4.0.tgz",
+      "integrity": "sha512-oYp7156SP8LkeGD0GF85ad1X9Ai79WtRsZ2gxJqtBuzH+98YUV6jkHEKlZkMbcrjJjIVJNIDP/3WL9wQkoPbWA==",
+      "engines": {
+        "node": ">=0.12"
+      },
+      "funding": {
+        "url": "https://github.com/fb55/entities?sponsor=1"
+      }
+    },
     "node_modules/envinfo": {
       "version": "7.8.1",
       "resolved": "https://registry.npmjs.org/envinfo/-/envinfo-7.8.1.tgz",
@@ -3920,6 +4140,11 @@
       "integrity": "sha512-lhd/wF+Lk98HZoTCtlVraHtfh5XYijIjalXck7saUtuanSDyLMxnHhSXEDJqHxD7msR8D0uCmqlkwjCV8xvwHw==",
       "dev": true
     },
+    "node_modules/fast-plist": {
+      "version": "0.1.3",
+      "resolved": "https://registry.npmjs.org/fast-plist/-/fast-plist-0.1.3.tgz",
+      "integrity": "sha512-d9cEfo/WcOezgPLAC/8t8wGb6YOD6JTCPMw2QcG2nAdFmyY+9rTUizCTaGjIZAloWENTEUMAPpkUAIJJJ0i96A=="
+    },
     "node_modules/fastest-levenshtein": {
       "version": "1.0.16",
       "resolved": "https://registry.npmjs.org/fastest-levenshtein/-/fastest-levenshtein-1.0.16.tgz",
@@ -3941,6 +4166,11 @@
         "node": ">=0.8.0"
       }
     },
+    "node_modules/file-saver": {
+      "version": "2.0.5",
+      "resolved": "https://registry.npmjs.org/file-saver/-/file-saver-2.0.5.tgz",
+      "integrity": "sha512-P9bmyZ3h/PRG+Nzga+rbdI4OEpNDzAVyy74uVO9ATgzLK6VtAsYybF/+TOCvrc0MO793d6+42lLyZTw7/ArVzA=="
+    },
     "node_modules/fill-range": {
       "version": "7.0.1",
       "resolved": "https://registry.npmjs.org/fill-range/-/fill-range-7.0.1.tgz",
@@ -4027,7 +4257,6 @@
       "version": "1.15.2",
       "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.15.2.tgz",
       "integrity": "sha512-VQLG33o04KaQ8uYi2tVNbdrWp1QWxNNea+nmIB4EVM28v0hmP17z7aG1+wAkNzVq4KeXTq3221ye5qTJP91JwA==",
-      "dev": true,
       "funding": [
         {
           "type": "individual",
@@ -4267,6 +4496,24 @@
       "integrity": "sha512-DV5Ln36z34NNTDgnz0EWGBLZENelNAtkiFA4kyNOG2tDI6Mz1uSWiq1wAKdyjnJwyDiDO7Fa2SO1CTxPXL8VxA==",
       "dev": true
     },
+    "node_modules/htmlparser2": {
+      "version": "8.0.1",
+      "resolved": "https://registry.npmjs.org/htmlparser2/-/htmlparser2-8.0.1.tgz",
+      "integrity": "sha512-4lVbmc1diZC7GUJQtRQ5yBAeUCL1exyMwmForWkRLnwyzWBFxN633SALPMGYaWZvKe9j1pRZJpauvmxENSp/EA==",
+      "funding": [
+        "https://github.com/fb55/htmlparser2?sponsor=1",
+        {
+          "type": "github",
+          "url": "https://github.com/sponsors/fb55"
+        }
+      ],
+      "dependencies": {
+        "domelementtype": "^2.3.0",
+        "domhandler": "^5.0.2",
+        "domutils": "^3.0.1",
+        "entities": "^4.3.0"
+      }
+    },
     "node_modules/http-deceiver": {
       "version": "1.2.7",
       "resolved": "https://registry.npmjs.org/http-deceiver/-/http-deceiver-1.2.7.tgz",
@@ -4437,6 +4684,11 @@
         "loose-envify": "^1.0.0"
       }
     },
+    "node_modules/ip-anonymize": {
+      "version": "0.1.0",
+      "resolved": "https://registry.npmjs.org/ip-anonymize/-/ip-anonymize-0.1.0.tgz",
+      "integrity": "sha512-cZJu+N5JKKFGMK0eEQWNaQMn2EhCysciVM6eotCJwfqotj16BTfVchKsJCH6mQAT9N0GC7oWRcsZ6Lb8dDiwTA=="
+    },
     "node_modules/ipaddr.js": {
       "version": "1.9.1",
       "resolved": "https://registry.npmjs.org/ipaddr.js/-/ipaddr.js-1.9.1.tgz",
@@ -4708,6 +4960,78 @@
         "node": ">=0.10.0"
       }
     },
+    "node_modules/lean4": {
+      "version": "0.0.95",
+      "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?a51db90",
+      "integrity": "sha512-eKDMAR/1LvozI+Zhw4smMerwhYi2aZR1Yf0v5jbxu3g5z4YMMhYJpYhbtVhf4Za0boSsol2+z2dxc8fBI/1LOg==",
+      "license": "Apache-2.0",
+      "dependencies": {
+        "@esm-bundle/react": "^17.0.2-fix.1",
+        "@esm-bundle/react-dom": "^17.0.2-fix.0",
+        "@leanprover/infoview": "^0.2.0",
+        "@leanprover/infoview-api": "^0.1.0",
+        "axios": "^0.24.0",
+        "cheerio": "^1.0.0-rc.10",
+        "mobx": "5.15.7",
+        "semver": "=7.3.5",
+        "vscode-languageclient": "=8.0.2"
+      },
+      "engines": {
+        "vscode": "^1.70.0"
+      }
+    },
+    "node_modules/lean4/node_modules/mobx": {
+      "version": "5.15.7",
+      "resolved": "https://registry.npmjs.org/mobx/-/mobx-5.15.7.tgz",
+      "integrity": "sha512-wyM3FghTkhmC+hQjyPGGFdpehrcX1KOXsDuERhfK2YbJemkUhEB+6wzEN639T21onxlfYBmriA1PFnvxTUhcKw==",
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/mobx"
+      }
+    },
+    "node_modules/lean4/node_modules/semver": {
+      "version": "7.3.5",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-7.3.5.tgz",
+      "integrity": "sha512-PoeGJYh8HK4BTO/a9Tf6ZG3veo/A7ZVsYrSA6J8ny9nb3B1VrpkuN+z9OE5wfE5p6H4LchYZsegiQgbJD94ZFQ==",
+      "dependencies": {
+        "lru-cache": "^6.0.0"
+      },
+      "bin": {
+        "semver": "bin/semver.js"
+      },
+      "engines": {
+        "node": ">=10"
+      }
+    },
+    "node_modules/lean4web": {
+      "version": "0.1.0",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#3be4ce778bbd7507876d5414dc99f5d44a60a274",
+      "dependencies": {
+        "@fontsource/roboto": "^4.5.8",
+        "@fontsource/roboto-mono": "^4.5.8",
+        "@fortawesome/fontawesome-svg-core": "^6.2.0",
+        "@fortawesome/free-solid-svg-icons": "^6.2.0",
+        "@fortawesome/react-fontawesome": "^0.2.0",
+        "@leanprover/infoview": "git+https://github.com/abentkamp/infoview-npm.git",
+        "express": "^4.18.2",
+        "file-saver": "^2.0.5",
+        "ip-anonymize": "^0.1.0",
+        "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?a51db90",
+        "mobx": "^6.6.2",
+        "monaco-editor": "^0.34.1",
+        "monaco-editor-textmate": "^4.0.0",
+        "monaco-languageclient": "^4.0.1",
+        "monaco-textmate": "^3.0.1",
+        "onigasm": "^2.2.5",
+        "path-browserify": "^1.0.1",
+        "react": "^18.2.0",
+        "react-dom": "^18.2.0",
+        "react-split": "^2.0.14",
+        "stream-http": "^3.2.0",
+        "vscode-ws-jsonrpc": "^2.0.0",
+        "ws": "^8.9.0"
+      }
+    },
     "node_modules/lines-and-columns": {
       "version": "1.2.4",
       "resolved": "https://registry.npmjs.org/lines-and-columns/-/lines-and-columns-1.2.4.tgz",
@@ -4774,7 +5098,6 @@
       "version": "6.0.0",
       "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz",
       "integrity": "sha512-Jo6dJ04CmSjuznwJSS3pUeWmd/H0ffTlkXXgwZi+eq1UCmqQwCh+eLsYOYCwY991i2Fah4h1BEMCx4qThGbsiA==",
-      "dev": true,
       "dependencies": {
         "yallist": "^4.0.0"
       },
@@ -4806,6 +5129,17 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
+    "node_modules/marked": {
+      "version": "4.2.3",
+      "resolved": "https://registry.npmjs.org/marked/-/marked-4.2.3.tgz",
+      "integrity": "sha512-slWRdJkbTZ+PjkyJnE30Uid64eHwbwa1Q25INCAYfZlK4o6ylagBy/Le9eWntqJFoFT93ikUKMv47GZ4gTwHkw==",
+      "bin": {
+        "marked": "bin/marked.js"
+      },
+      "engines": {
+        "node": ">= 12"
+      }
+    },
     "node_modules/mathjax-full": {
       "version": "3.2.2",
       "resolved": "https://registry.npmjs.org/mathjax-full/-/mathjax-full-3.2.2.tgz",
@@ -5411,7 +5745,6 @@
       "version": "3.1.2",
       "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-3.1.2.tgz",
       "integrity": "sha512-J7p63hRiAjw1NDEww1W7i37+ByIrOWO5XQQAzZ3VOcL0PNybwpfmV/N05zFAzwQ9USyEcX6t3UO+K5aqBQOIHw==",
-      "dev": true,
       "dependencies": {
         "brace-expansion": "^1.1.7"
       },
@@ -5424,6 +5757,54 @@
       "resolved": "https://registry.npmjs.org/mj-context-menu/-/mj-context-menu-0.6.1.tgz",
       "integrity": "sha512-7NO5s6n10TIV96d4g2uDpG7ZDpIhMh0QNfGdJw/W47JswFcosz457wqz/b5sAKvl12sxINGFCn80NZHKwxQEXA=="
     },
+    "node_modules/mobx": {
+      "version": "6.7.0",
+      "resolved": "https://registry.npmjs.org/mobx/-/mobx-6.7.0.tgz",
+      "integrity": "sha512-1kBLBdSNG2bA522HQdbsTvwAwYf9hq9FWxmlhX7wTsJUAI54907J+ozfGW+LoYUo06vjit748g6QH1AAGLNebw==",
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/mobx"
+      }
+    },
+    "node_modules/monaco-editor": {
+      "version": "0.34.1",
+      "resolved": "https://registry.npmjs.org/monaco-editor/-/monaco-editor-0.34.1.tgz",
+      "integrity": "sha512-FKc80TyiMaruhJKKPz5SpJPIjL+dflGvz4CpuThaPMc94AyN7SeC9HQ8hrvaxX7EyHdJcUY5i4D0gNyJj1vSZQ=="
+    },
+    "node_modules/monaco-editor-textmate": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/monaco-editor-textmate/-/monaco-editor-textmate-4.0.0.tgz",
+      "integrity": "sha512-Clwup5LJzVfwURQrS+odSEC5/hZBEG36pQnvBKt4OtBndF8r2xLeXUZcK/AqEBK2u0Npy7frFp9hG7m66Ol9hA==",
+      "peerDependencies": {
+        "monaco-editor": "0.x.x",
+        "monaco-textmate": "^3.0.0"
+      }
+    },
+    "node_modules/monaco-languageclient": {
+      "version": "4.0.1",
+      "resolved": "https://registry.npmjs.org/monaco-languageclient/-/monaco-languageclient-4.0.1.tgz",
+      "integrity": "sha512-mUIq/7gQM/8CyOBVGv0thLRAR80vk49Ur0ROJveoh6R0/uwaUoyri+5OBslxsa5BICftLTsC8/Y+at6/iW50Ww==",
+      "dependencies": {
+        "vscode": "npm:@codingame/monaco-vscode-api@1.69.12",
+        "vscode-jsonrpc": "8.0.2",
+        "vscode-languageclient": "8.0.2"
+      },
+      "engines": {
+        "node": ">=16.11.0",
+        "npm": ">=8.0.0"
+      }
+    },
+    "node_modules/monaco-textmate": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/monaco-textmate/-/monaco-textmate-3.0.1.tgz",
+      "integrity": "sha512-ZxxY3OsqUczYP1sGqo97tu+CJmMBwuSW+dL0WEBdDhOZ5G1zntw72hvBc68ZQAirosWvbDKgN1dL5k173QtFww==",
+      "dependencies": {
+        "fast-plist": "^0.1.2"
+      },
+      "peerDependencies": {
+        "onigasm": "^2.0.0"
+      }
+    },
     "node_modules/mri": {
       "version": "1.2.0",
       "resolved": "https://registry.npmjs.org/mri/-/mri-1.2.0.tgz",
@@ -5573,6 +5954,17 @@
         "node": ">=8"
       }
     },
+    "node_modules/nth-check": {
+      "version": "2.1.1",
+      "resolved": "https://registry.npmjs.org/nth-check/-/nth-check-2.1.1.tgz",
+      "integrity": "sha512-lqjrjmaOoAnWfMmBPL+XNnynZh2+swxiX3WUE0s4yEHI6m+AwrK2UZOimIRl3X/4QctVqS8AiZjFqyOGrMXb/w==",
+      "dependencies": {
+        "boolbase": "^1.0.0"
+      },
+      "funding": {
+        "url": "https://github.com/fb55/nth-check?sponsor=1"
+      }
+    },
     "node_modules/object-assign": {
       "version": "4.1.1",
       "resolved": "https://registry.npmjs.org/object-assign/-/object-assign-4.1.1.tgz",
@@ -5666,6 +6058,27 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
+    "node_modules/onigasm": {
+      "version": "2.2.5",
+      "resolved": "https://registry.npmjs.org/onigasm/-/onigasm-2.2.5.tgz",
+      "integrity": "sha512-F+th54mPc0l1lp1ZcFMyL/jTs2Tlq4SqIHKIXGZOR/VkHkF9A7Fr5rRr5+ZG/lWeRsyrClLYRq7s/yFQ/XhWCA==",
+      "dependencies": {
+        "lru-cache": "^5.1.1"
+      }
+    },
+    "node_modules/onigasm/node_modules/lru-cache": {
+      "version": "5.1.1",
+      "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-5.1.1.tgz",
+      "integrity": "sha512-KpNARQA3Iwv+jTA0utUVVbrh+Jlrr1Fv0e56GGzAFOXN7dk/FviaDW8LHmK52DlcH4WP2n6gI8vN1aesBFgo9w==",
+      "dependencies": {
+        "yallist": "^3.0.2"
+      }
+    },
+    "node_modules/onigasm/node_modules/yallist": {
+      "version": "3.1.1",
+      "resolved": "https://registry.npmjs.org/yallist/-/yallist-3.1.1.tgz",
+      "integrity": "sha512-a4UGQaWPH59mOXUYnAG2ewncQS4i4F43Tv3JoAM+s2VDAmS9NsK8GpDMLrCHPksFT7h3K6TOoUNn2pb7RoXx4g=="
+    },
     "node_modules/open": {
       "version": "8.4.0",
       "resolved": "https://registry.npmjs.org/open/-/open-8.4.0.tgz",
@@ -5767,6 +6180,29 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
+    "node_modules/parse5": {
+      "version": "7.1.2",
+      "resolved": "https://registry.npmjs.org/parse5/-/parse5-7.1.2.tgz",
+      "integrity": "sha512-Czj1WaSVpaoj0wbhMzLmWD69anp2WH7FXMB9n1Sy8/ZFF9jolSQVMu1Ij5WIyGmcBmhk7EOndpO4mIpihVqAXw==",
+      "dependencies": {
+        "entities": "^4.4.0"
+      },
+      "funding": {
+        "url": "https://github.com/inikulin/parse5?sponsor=1"
+      }
+    },
+    "node_modules/parse5-htmlparser2-tree-adapter": {
+      "version": "7.0.0",
+      "resolved": "https://registry.npmjs.org/parse5-htmlparser2-tree-adapter/-/parse5-htmlparser2-tree-adapter-7.0.0.tgz",
+      "integrity": "sha512-B77tOZrqqfUfnVcOrUvfdLbz4pu4RopLD/4vmu3HUPswwTA8OH0EMW9BlWR2B0RCoiZRAHEUu7IxeP1Pd1UU+g==",
+      "dependencies": {
+        "domhandler": "^5.0.2",
+        "parse5": "^7.0.0"
+      },
+      "funding": {
+        "url": "https://github.com/inikulin/parse5?sponsor=1"
+      }
+    },
     "node_modules/parseurl": {
       "version": "1.3.3",
       "resolved": "https://registry.npmjs.org/parseurl/-/parseurl-1.3.3.tgz",
@@ -5775,6 +6211,11 @@
         "node": ">= 0.8"
       }
     },
+    "node_modules/path-browserify": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/path-browserify/-/path-browserify-1.0.1.tgz",
+      "integrity": "sha512-b7uo2UCUOYZcnF/3ID0lulOJi/bafxa1xPe7ZPsammBSpjSWQkjNxlt635YGS2MiR9GjvuXCtz2emr3jbsz98g=="
+    },
     "node_modules/path-exists": {
       "version": "4.0.0",
       "resolved": "https://registry.npmjs.org/path-exists/-/path-exists-4.0.0.tgz",
@@ -6173,6 +6614,11 @@
         "react": "^18.2.0"
       }
     },
+    "node_modules/react-fast-compare": {
+      "version": "3.2.0",
+      "resolved": "https://registry.npmjs.org/react-fast-compare/-/react-fast-compare-3.2.0.tgz",
+      "integrity": "sha512-rtGImPZ0YyLrscKI9xTpV8psd6I8VAtjKCzQDlzyDvqJA8XOW78TXYQwNRNd8g8JZnDu8q9Fu/1v4HPAVwVdHA=="
+    },
     "node_modules/react-is": {
       "version": "18.2.0",
       "resolved": "https://registry.npmjs.org/react-is/-/react-is-18.2.0.tgz",
@@ -6217,6 +6663,18 @@
         "node": ">=0.10.0"
       }
     },
+    "node_modules/react-split": {
+      "version": "2.0.14",
+      "resolved": "https://registry.npmjs.org/react-split/-/react-split-2.0.14.tgz",
+      "integrity": "sha512-bKWydgMgaKTg/2JGQnaJPg51T6dmumTWZppFgEbbY0Fbme0F5TuatAScCLaqommbGQQf/ZT1zaejuPDriscISA==",
+      "dependencies": {
+        "prop-types": "^15.5.7",
+        "split.js": "^1.6.0"
+      },
+      "peerDependencies": {
+        "react": "*"
+      }
+    },
     "node_modules/react-transition-group": {
       "version": "4.4.5",
       "resolved": "https://registry.npmjs.org/react-transition-group/-/react-transition-group-4.4.5.tgz",
@@ -6929,6 +7387,11 @@
         "node": "^12.20.0 || >=14"
       }
     },
+    "node_modules/split.js": {
+      "version": "1.6.5",
+      "resolved": "https://registry.npmjs.org/split.js/-/split.js-1.6.5.tgz",
+      "integrity": "sha512-mPTnGCiS/RiuTNsVhCm9De9cCAUsrNFFviRbADdKiiV+Kk8HKp/0fWu7Kr8pi3/yBmsqLFHuXGT9UUZ+CNLwFw=="
+    },
     "node_modules/stackframe": {
       "version": "1.3.4",
       "resolved": "https://registry.npmjs.org/stackframe/-/stackframe-1.3.4.tgz",
@@ -6943,11 +7406,34 @@
         "node": ">= 0.8"
       }
     },
+    "node_modules/stream-http": {
+      "version": "3.2.0",
+      "resolved": "https://registry.npmjs.org/stream-http/-/stream-http-3.2.0.tgz",
+      "integrity": "sha512-Oq1bLqisTyK3TSCXpPbT4sdeYNdmyZJv1LxpEm2vu1ZhK89kSE5YXwZc3cWk0MagGaKriBh9mCFbVGtO+vY29A==",
+      "dependencies": {
+        "builtin-status-codes": "^3.0.0",
+        "inherits": "^2.0.4",
+        "readable-stream": "^3.6.0",
+        "xtend": "^4.0.2"
+      }
+    },
+    "node_modules/stream-http/node_modules/readable-stream": {
+      "version": "3.6.0",
+      "resolved": "https://registry.npmjs.org/readable-stream/-/readable-stream-3.6.0.tgz",
+      "integrity": "sha512-BViHy7LKeTz4oNnkcLJ+lVSL6vpiFeX6/d3oSH8zCW7UxP2onchk+vTGB143xuFjHS3deTgkKoXXymXqymiIdA==",
+      "dependencies": {
+        "inherits": "^2.0.3",
+        "string_decoder": "^1.1.1",
+        "util-deprecate": "^1.0.1"
+      },
+      "engines": {
+        "node": ">= 6"
+      }
+    },
     "node_modules/string_decoder": {
       "version": "1.3.0",
       "resolved": "https://registry.npmjs.org/string_decoder/-/string_decoder-1.3.0.tgz",
       "integrity": "sha512-hkRX8U1WjJFd8LsDJ2yQ/wWWxaopEsABU1XfkM8A+j0+85JAGppt16cr1Whg6KIbb4okU6Mql6BOj+uup/wKeA==",
-      "dev": true,
       "dependencies": {
         "safe-buffer": "~5.2.0"
       }
@@ -7026,6 +7512,11 @@
         "url": "https://github.com/sponsors/ljharb"
       }
     },
+    "node_modules/tachyons": {
+      "version": "4.12.0",
+      "resolved": "https://registry.npmjs.org/tachyons/-/tachyons-4.12.0.tgz",
+      "integrity": "sha512-2nA2IrYFy3raCM9fxJ2KODRGHVSZNTW3BR0YnlGsLUf1DA3pk3YfWZ/DdfbnZK6zLZS+jUenlUGJsKcA5fUiZg=="
+    },
     "node_modules/tapable": {
       "version": "2.2.1",
       "resolved": "https://registry.npmjs.org/tapable/-/tapable-2.2.1.tgz",
@@ -7487,8 +7978,7 @@
     "node_modules/util-deprecate": {
       "version": "1.0.2",
       "resolved": "https://registry.npmjs.org/util-deprecate/-/util-deprecate-1.0.2.tgz",
-      "integrity": "sha512-EPD5q1uXyFxJpCrLnCc1nHnq3gOa6DZBocAIiI2TaSCA7VCJ1UJDMagCzIkXNsUYfD1daK//LTEQ8xiIbrHtcw==",
-      "dev": true
+      "integrity": "sha512-EPD5q1uXyFxJpCrLnCc1nHnq3gOa6DZBocAIiI2TaSCA7VCJ1UJDMagCzIkXNsUYfD1daK//LTEQ8xiIbrHtcw=="
     },
     "node_modules/utils-merge": {
       "version": "1.0.1",
@@ -7568,6 +8058,19 @@
         "url": "https://opencollective.com/unified"
       }
     },
+    "node_modules/vscode": {
+      "name": "@codingame/monaco-vscode-api",
+      "version": "1.69.12",
+      "resolved": "https://registry.npmjs.org/@codingame/monaco-vscode-api/-/monaco-vscode-api-1.69.12.tgz",
+      "integrity": "sha512-ES1xRnU232t82tcdM2ImikkjGfAMgJtrF0XkLa4poEnvcUH0SFqUhYvcqk5CFggQWh16jqxifVvozcu0/mbH7A==",
+      "dependencies": {
+        "monaco-editor": "^0.34.0"
+      },
+      "peerDependencies": {
+        "vscode-oniguruma": "^1.6.2",
+        "vscode-textmate": "^7.0.1"
+      }
+    },
     "node_modules/vscode-jsonrpc": {
       "version": "8.0.2",
       "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-8.0.2.tgz",
@@ -7576,6 +8079,59 @@
         "node": ">=14.0.0"
       }
     },
+    "node_modules/vscode-languageclient": {
+      "version": "8.0.2",
+      "resolved": "https://registry.npmjs.org/vscode-languageclient/-/vscode-languageclient-8.0.2.tgz",
+      "integrity": "sha512-lHlthJtphG9gibGb/y72CKqQUxwPsMXijJVpHEC2bvbFqxmkj9LwQ3aGU9dwjBLqsX1S4KjShYppLvg1UJDF/Q==",
+      "dependencies": {
+        "minimatch": "^3.0.4",
+        "semver": "^7.3.5",
+        "vscode-languageserver-protocol": "3.17.2"
+      },
+      "engines": {
+        "vscode": "^1.67.0"
+      }
+    },
+    "node_modules/vscode-languageclient/node_modules/semver": {
+      "version": "7.3.8",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-7.3.8.tgz",
+      "integrity": "sha512-NB1ctGL5rlHrPJtFDVIVzTyQylMLu9N9VICA6HSFJo8MCGVTMW6gfpicwKmmK/dAjTOrqu5l63JJOpDSrAis3A==",
+      "dependencies": {
+        "lru-cache": "^6.0.0"
+      },
+      "bin": {
+        "semver": "bin/semver.js"
+      },
+      "engines": {
+        "node": ">=10"
+      }
+    },
+    "node_modules/vscode-languageserver-protocol": {
+      "version": "3.17.2",
+      "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.17.2.tgz",
+      "integrity": "sha512-8kYisQ3z/SQ2kyjlNeQxbkkTNmVFoQCqkmGrzLH6A9ecPlgTbp3wDTnUNqaUxYr4vlAcloxx8zwy7G5WdguYNg==",
+      "dependencies": {
+        "vscode-jsonrpc": "8.0.2",
+        "vscode-languageserver-types": "3.17.2"
+      }
+    },
+    "node_modules/vscode-languageserver-types": {
+      "version": "3.17.2",
+      "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.17.2.tgz",
+      "integrity": "sha512-zHhCWatviizPIq9B7Vh9uvrH6x3sK8itC84HkamnBWoDFJtzBf7SWlpLCZUit72b3os45h6RWQNC9xHRDF8dRA=="
+    },
+    "node_modules/vscode-oniguruma": {
+      "version": "1.6.2",
+      "resolved": "https://registry.npmjs.org/vscode-oniguruma/-/vscode-oniguruma-1.6.2.tgz",
+      "integrity": "sha512-KH8+KKov5eS/9WhofZR8M8dMHWN2gTxjMsG4jd04YhpbPR91fUj7rYQ2/XjeHCJWbg7X++ApRIU9NUwM2vTvLA==",
+      "peer": true
+    },
+    "node_modules/vscode-textmate": {
+      "version": "7.0.3",
+      "resolved": "https://registry.npmjs.org/vscode-textmate/-/vscode-textmate-7.0.3.tgz",
+      "integrity": "sha512-OkE/mYm1h5ZX9IEKeKR/2zKDt2SzYyIfTEOVFX4QhA+B3BPROvNEmDDXvBThz3qknKO3Cy/VVb8/sx1UlqP/Xw==",
+      "peer": true
+    },
     "node_modules/vscode-ws-jsonrpc": {
       "version": "2.0.0",
       "resolved": "https://registry.npmjs.org/vscode-ws-jsonrpc/-/vscode-ws-jsonrpc-2.0.0.tgz",
@@ -8060,11 +8616,18 @@
         "node": ">=0.1"
       }
     },
+    "node_modules/xtend": {
+      "version": "4.0.2",
+      "resolved": "https://registry.npmjs.org/xtend/-/xtend-4.0.2.tgz",
+      "integrity": "sha512-LKYU1iAXJXUgAXn9URjiu+MWhyUXHsvfp7mcuYm9dSUKK0/CjtrUwFAxD82/mCWbtLsGjFIad0wIsod4zrTAEQ==",
+      "engines": {
+        "node": ">=0.4"
+      }
+    },
     "node_modules/yallist": {
       "version": "4.0.0",
       "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz",
-      "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A==",
-      "dev": true
+      "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A=="
     },
     "node_modules/yaml": {
       "version": "1.10.2",
@@ -9152,6 +9715,16 @@
       "resolved": "https://registry.npmjs.org/@emotion/weak-memoize/-/weak-memoize-0.3.0.tgz",
       "integrity": "sha512-AHPmaAx+RYfZz0eYu6Gviiagpmiyw98ySSlQvCUhVGDRtDFe4DBS0x1bSjdF3gqUDYOczB+yYvBTtEylYSdRhg=="
     },
+    "@esm-bundle/react": {
+      "version": "17.0.2-fix.1",
+      "resolved": "https://registry.npmjs.org/@esm-bundle/react/-/react-17.0.2-fix.1.tgz",
+      "integrity": "sha512-AzHd8Hi5KQjwgU2e3SD1XrMm5WF8y8zsKmP9ttsyR6bzTS8TAc1mWRc8UW0Q/px4D38mcP4+ofJDAhhFiB7KXg=="
+    },
+    "@esm-bundle/react-dom": {
+      "version": "17.0.2-fix.0",
+      "resolved": "https://registry.npmjs.org/@esm-bundle/react-dom/-/react-dom-17.0.2-fix.0.tgz",
+      "integrity": "sha512-U0ofefDbwOtgBh3kOAXklRoYDN9COtjVFiQ8aW7/H8FmBi96S8PYtm4xObITSqjDfvZOWC4Z1g1p3zsgBr8PGw=="
+    },
     "@fontsource/roboto": {
       "version": "4.5.8",
       "resolved": "https://registry.npmjs.org/@fontsource/roboto/-/roboto-4.5.8.tgz",
@@ -9162,6 +9735,35 @@
       "resolved": "https://registry.npmjs.org/@fontsource/roboto-mono/-/roboto-mono-4.5.8.tgz",
       "integrity": "sha512-AW44UkbQD0w1CT5mzDbsvhGZ6/bb0YmZzoELj6Sx8vcVEzcbYGUdt2Dtl5zqlOuYMWQFY1mniwWyVv+Bm/lVxw=="
     },
+    "@fortawesome/fontawesome-common-types": {
+      "version": "6.2.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.2.1.tgz",
+      "integrity": "sha512-Sz07mnQrTekFWLz5BMjOzHl/+NooTdW8F8kDQxjWwbpOJcnoSg4vUDng8d/WR1wOxM0O+CY9Zw0nR054riNYtQ=="
+    },
+    "@fortawesome/fontawesome-svg-core": {
+      "version": "6.2.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.2.1.tgz",
+      "integrity": "sha512-HELwwbCz6C1XEcjzyT1Jugmz2NNklMrSPjZOWMlc+ZsHIVk+XOvOXLGGQtFBwSyqfJDNgRq4xBCwWOaZ/d9DEA==",
+      "requires": {
+        "@fortawesome/fontawesome-common-types": "6.2.1"
+      }
+    },
+    "@fortawesome/free-solid-svg-icons": {
+      "version": "6.2.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.2.1.tgz",
+      "integrity": "sha512-oKuqrP5jbfEPJWTij4sM+/RvgX+RMFwx3QZCZcK9PrBDgxC35zuc7AOFsyMjMd/PIFPeB2JxyqDr5zs/DZFPPw==",
+      "requires": {
+        "@fortawesome/fontawesome-common-types": "6.2.1"
+      }
+    },
+    "@fortawesome/react-fontawesome": {
+      "version": "0.2.0",
+      "resolved": "https://registry.npmjs.org/@fortawesome/react-fontawesome/-/react-fontawesome-0.2.0.tgz",
+      "integrity": "sha512-uHg75Rb/XORTtVt7OS9WoK8uM276Ufi7gCzshVWkUJbHhh3svsUUeqXerrM96Wm7fRiDzfKRwSoahhMIkGAYHw==",
+      "requires": {
+        "prop-types": "^15.8.1"
+      }
+    },
     "@jridgewell/gen-mapping": {
       "version": "0.3.2",
       "resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.2.tgz",
@@ -9211,6 +9813,23 @@
         "@jridgewell/sourcemap-codec": "1.4.14"
       }
     },
+    "@leanprover/infoview": {
+      "version": "git+ssh://git@github.com/abentkamp/infoview-npm.git#eb2e3982eded7f7f45fe245a5b20c4804fb82079",
+      "from": "@leanprover/infoview@^0.2.0",
+      "requires": {
+        "@leanprover/infoview-api": "^0.1.0",
+        "@vscode/codicons": "0.0.28",
+        "marked": "^4.0.17",
+        "react-fast-compare": "^3.2.0",
+        "tachyons": "^4.12.0",
+        "vscode-languageserver-protocol": "^3.17.2"
+      }
+    },
+    "@leanprover/infoview-api": {
+      "version": "0.1.0",
+      "resolved": "https://registry.npmjs.org/@leanprover/infoview-api/-/infoview-api-0.1.0.tgz",
+      "integrity": "sha512-vNMFrk5U1UlWhHp7G1e33mG7hJHyIErb3INgsVITbEW8CzOlAUrc83Pp3ARZykIc8++WJhT7WH+lALo8nO7G0Q=="
+    },
     "@leichtgewicht/ip-codec": {
       "version": "2.0.4",
       "resolved": "https://registry.npmjs.org/@leichtgewicht/ip-codec/-/ip-codec-2.0.4.tgz",
@@ -9694,6 +10313,11 @@
         "@types/node": "*"
       }
     },
+    "@vscode/codicons": {
+      "version": "0.0.28",
+      "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.28.tgz",
+      "integrity": "sha512-p8zph8Tflh6KUirDCVOti8tr/BhngQx9Z6QXSKBJgPTZMxiKmP6eF75AKDopUeffp7X80Vdo48nv4kdW9d73Dg=="
+    },
     "@webassemblyjs/ast": {
       "version": "1.11.1",
       "resolved": "https://registry.npmjs.org/@webassemblyjs/ast/-/ast-1.11.1.tgz",
@@ -9993,6 +10617,14 @@
       "resolved": "https://registry.npmjs.org/array-flatten/-/array-flatten-1.1.1.tgz",
       "integrity": "sha512-PCVAQswWemu6UdxsDFFX/+gVeYqKAod3D3UVm91jHwynguOwAvYPhx8nNlM++NqRcK6CxxpUafjmhIdKiHibqg=="
     },
+    "axios": {
+      "version": "0.24.0",
+      "resolved": "https://registry.npmjs.org/axios/-/axios-0.24.0.tgz",
+      "integrity": "sha512-Q6cWsys88HoPgAaFAVUb0WpPk0O8iTeisR9IMqy9G8AbO4NlpVknrnQS03zzF9PGAWgO3cgletO3VjV/P7VztA==",
+      "requires": {
+        "follow-redirects": "^1.14.4"
+      }
+    },
     "babel-loader": {
       "version": "8.2.5",
       "resolved": "https://registry.npmjs.org/babel-loader/-/babel-loader-8.2.5.tgz",
@@ -10047,8 +10679,7 @@
     "balanced-match": {
       "version": "1.0.2",
       "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.2.tgz",
-      "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw==",
-      "dev": true
+      "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw=="
     },
     "batch": {
       "version": "0.6.1",
@@ -10130,11 +10761,15 @@
         }
       }
     },
+    "boolbase": {
+      "version": "1.0.0",
+      "resolved": "https://registry.npmjs.org/boolbase/-/boolbase-1.0.0.tgz",
+      "integrity": "sha512-JZOSA7Mo9sNGB8+UjSgzdLtokWAky1zbztM3WRLCbZ70/3cTANmQmOdR7y2g+J0e2WXywy1yS468tY+IruqEww=="
+    },
     "brace-expansion": {
       "version": "1.1.11",
       "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.11.tgz",
       "integrity": "sha512-iCuPHDFgrHX7H2vEI/5xpz07zSHB00TpugqhmYtVmMO6518mCuRMoOYFldEBl0g187ufozdaHgWKcYFb61qGiA==",
-      "dev": true,
       "requires": {
         "balanced-match": "^1.0.0",
         "concat-map": "0.0.1"
@@ -10167,6 +10802,11 @@
       "integrity": "sha512-E+XQCRwSbaaiChtv6k6Dwgc+bx+Bs6vuKJHHl5kox/BaKbhiXzqQOwK4cO22yElGp2OCmjwVhT3HmxgyPGnJfQ==",
       "dev": true
     },
+    "builtin-status-codes": {
+      "version": "3.0.0",
+      "resolved": "https://registry.npmjs.org/builtin-status-codes/-/builtin-status-codes-3.0.0.tgz",
+      "integrity": "sha512-HpGFw18DgFWlncDfjTa2rcQ4W88O1mC8e8yZ2AvQY5KDaktSTwo+KRf6nHK6FRI5FyRyb/5T6+TSxfP7QyGsmQ=="
+    },
     "bytes": {
       "version": "3.1.2",
       "resolved": "https://registry.npmjs.org/bytes/-/bytes-3.1.2.tgz",
@@ -10218,6 +10858,33 @@
       "resolved": "https://registry.npmjs.org/character-entities/-/character-entities-2.0.2.tgz",
       "integrity": "sha512-shx7oQ0Awen/BRIdkjkvz54PnEEI/EjwXDSIZp86/KKdbafHh1Df/RYGBhn4hbe2+uKC9FnT5UCEdyPz3ai9hQ=="
     },
+    "cheerio": {
+      "version": "1.0.0-rc.12",
+      "resolved": "https://registry.npmjs.org/cheerio/-/cheerio-1.0.0-rc.12.tgz",
+      "integrity": "sha512-VqR8m68vM46BNnuZ5NtnGBKIE/DfN0cRIzg9n40EIq9NOv90ayxLBXA8fXC5gquFRGJSTRqBq25Jt2ECLR431Q==",
+      "requires": {
+        "cheerio-select": "^2.1.0",
+        "dom-serializer": "^2.0.0",
+        "domhandler": "^5.0.3",
+        "domutils": "^3.0.1",
+        "htmlparser2": "^8.0.1",
+        "parse5": "^7.0.0",
+        "parse5-htmlparser2-tree-adapter": "^7.0.0"
+      }
+    },
+    "cheerio-select": {
+      "version": "2.1.0",
+      "resolved": "https://registry.npmjs.org/cheerio-select/-/cheerio-select-2.1.0.tgz",
+      "integrity": "sha512-9v9kG0LvzrlcungtnJtpGNxY+fzECQKhK4EGJX2vByejiMX84MFNQw4UxPJl3bFbTMw+Dfs37XaIkCwTZfLh4g==",
+      "requires": {
+        "boolbase": "^1.0.0",
+        "css-select": "^5.1.0",
+        "css-what": "^6.1.0",
+        "domelementtype": "^2.3.0",
+        "domhandler": "^5.0.3",
+        "domutils": "^3.0.1"
+      }
+    },
     "chokidar": {
       "version": "3.5.3",
       "resolved": "https://registry.npmjs.org/chokidar/-/chokidar-3.5.3.tgz",
@@ -10356,8 +11023,7 @@
     "concat-map": {
       "version": "0.0.1",
       "resolved": "https://registry.npmjs.org/concat-map/-/concat-map-0.0.1.tgz",
-      "integrity": "sha512-/Srv4dswyQNBfohGpz9o6Yb3Gz3SrUDqBH5rTuhGR7ahtlbYKnVxw2bCFMRljaA7EXHaXZ8wsHdodFvbkhKmqg==",
-      "dev": true
+      "integrity": "sha512-/Srv4dswyQNBfohGpz9o6Yb3Gz3SrUDqBH5rTuhGR7ahtlbYKnVxw2bCFMRljaA7EXHaXZ8wsHdodFvbkhKmqg=="
     },
     "concurrently": {
       "version": "7.4.0",
@@ -10609,6 +11275,23 @@
         }
       }
     },
+    "css-select": {
+      "version": "5.1.0",
+      "resolved": "https://registry.npmjs.org/css-select/-/css-select-5.1.0.tgz",
+      "integrity": "sha512-nwoRF1rvRRnnCqqY7updORDsuqKzqYJ28+oSMaJMMgOauh3fvwHqMS7EZpIPqK8GL+g9mKxF1vP/ZjSeNjEVHg==",
+      "requires": {
+        "boolbase": "^1.0.0",
+        "css-what": "^6.1.0",
+        "domhandler": "^5.0.2",
+        "domutils": "^3.0.1",
+        "nth-check": "^2.0.1"
+      }
+    },
+    "css-what": {
+      "version": "6.1.0",
+      "resolved": "https://registry.npmjs.org/css-what/-/css-what-6.1.0.tgz",
+      "integrity": "sha512-HTUrgRJ7r4dsZKU6GjmpfRK1O76h97Z8MfS1G0FozR+oF2kG6Vfe8JE6zwrkbxigziPHinCJ+gCPjA9EaBDtRw=="
+    },
     "cssesc": {
       "version": "3.0.0",
       "resolved": "https://registry.npmjs.org/cssesc/-/cssesc-3.0.0.tgz",
@@ -10723,6 +11406,39 @@
         "csstype": "^3.0.2"
       }
     },
+    "dom-serializer": {
+      "version": "2.0.0",
+      "resolved": "https://registry.npmjs.org/dom-serializer/-/dom-serializer-2.0.0.tgz",
+      "integrity": "sha512-wIkAryiqt/nV5EQKqQpo3SToSOV9J0DnbJqwK7Wv/Trc92zIAYZ4FlMu+JPFW1DfGFt81ZTCGgDEabffXeLyJg==",
+      "requires": {
+        "domelementtype": "^2.3.0",
+        "domhandler": "^5.0.2",
+        "entities": "^4.2.0"
+      }
+    },
+    "domelementtype": {
+      "version": "2.3.0",
+      "resolved": "https://registry.npmjs.org/domelementtype/-/domelementtype-2.3.0.tgz",
+      "integrity": "sha512-OLETBj6w0OsagBwdXnPdN0cnMfF9opN69co+7ZrbfPGrdpPVNBUj02spi6B1N7wChLQiPn4CSH/zJvXw56gmHw=="
+    },
+    "domhandler": {
+      "version": "5.0.3",
+      "resolved": "https://registry.npmjs.org/domhandler/-/domhandler-5.0.3.tgz",
+      "integrity": "sha512-cgwlv/1iFQiFnU96XXgROh8xTeetsnJiDsTc7TYCLFd9+/WNkIqPTxiM/8pSd8VIrhXGTf1Ny1q1hquVqDJB5w==",
+      "requires": {
+        "domelementtype": "^2.3.0"
+      }
+    },
+    "domutils": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/domutils/-/domutils-3.0.1.tgz",
+      "integrity": "sha512-z08c1l761iKhDFtfXO04C7kTdPBLi41zwOZl00WS8b5eiaebNpY00HKbztwBq+e3vyqWNwWF3mP9YLUeqIrF+Q==",
+      "requires": {
+        "dom-serializer": "^2.0.0",
+        "domelementtype": "^2.3.0",
+        "domhandler": "^5.0.1"
+      }
+    },
     "ee-first": {
       "version": "1.1.1",
       "resolved": "https://registry.npmjs.org/ee-first/-/ee-first-1.1.1.tgz",
@@ -10761,6 +11477,11 @@
         "tapable": "^2.2.0"
       }
     },
+    "entities": {
+      "version": "4.4.0",
+      "resolved": "https://registry.npmjs.org/entities/-/entities-4.4.0.tgz",
+      "integrity": "sha512-oYp7156SP8LkeGD0GF85ad1X9Ai79WtRsZ2gxJqtBuzH+98YUV6jkHEKlZkMbcrjJjIVJNIDP/3WL9wQkoPbWA=="
+    },
     "envinfo": {
       "version": "7.8.1",
       "resolved": "https://registry.npmjs.org/envinfo/-/envinfo-7.8.1.tgz",
@@ -10952,6 +11673,11 @@
       "integrity": "sha512-lhd/wF+Lk98HZoTCtlVraHtfh5XYijIjalXck7saUtuanSDyLMxnHhSXEDJqHxD7msR8D0uCmqlkwjCV8xvwHw==",
       "dev": true
     },
+    "fast-plist": {
+      "version": "0.1.3",
+      "resolved": "https://registry.npmjs.org/fast-plist/-/fast-plist-0.1.3.tgz",
+      "integrity": "sha512-d9cEfo/WcOezgPLAC/8t8wGb6YOD6JTCPMw2QcG2nAdFmyY+9rTUizCTaGjIZAloWENTEUMAPpkUAIJJJ0i96A=="
+    },
     "fastest-levenshtein": {
       "version": "1.0.16",
       "resolved": "https://registry.npmjs.org/fastest-levenshtein/-/fastest-levenshtein-1.0.16.tgz",
@@ -10967,6 +11693,11 @@
         "websocket-driver": ">=0.5.1"
       }
     },
+    "file-saver": {
+      "version": "2.0.5",
+      "resolved": "https://registry.npmjs.org/file-saver/-/file-saver-2.0.5.tgz",
+      "integrity": "sha512-P9bmyZ3h/PRG+Nzga+rbdI4OEpNDzAVyy74uVO9ATgzLK6VtAsYybF/+TOCvrc0MO793d6+42lLyZTw7/ArVzA=="
+    },
     "fill-range": {
       "version": "7.0.1",
       "resolved": "https://registry.npmjs.org/fill-range/-/fill-range-7.0.1.tgz",
@@ -11036,8 +11767,7 @@
     "follow-redirects": {
       "version": "1.15.2",
       "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.15.2.tgz",
-      "integrity": "sha512-VQLG33o04KaQ8uYi2tVNbdrWp1QWxNNea+nmIB4EVM28v0hmP17z7aG1+wAkNzVq4KeXTq3221ye5qTJP91JwA==",
-      "dev": true
+      "integrity": "sha512-VQLG33o04KaQ8uYi2tVNbdrWp1QWxNNea+nmIB4EVM28v0hmP17z7aG1+wAkNzVq4KeXTq3221ye5qTJP91JwA=="
     },
     "forwarded": {
       "version": "0.2.0",
@@ -11212,6 +11942,17 @@
       "integrity": "sha512-DV5Ln36z34NNTDgnz0EWGBLZENelNAtkiFA4kyNOG2tDI6Mz1uSWiq1wAKdyjnJwyDiDO7Fa2SO1CTxPXL8VxA==",
       "dev": true
     },
+    "htmlparser2": {
+      "version": "8.0.1",
+      "resolved": "https://registry.npmjs.org/htmlparser2/-/htmlparser2-8.0.1.tgz",
+      "integrity": "sha512-4lVbmc1diZC7GUJQtRQ5yBAeUCL1exyMwmForWkRLnwyzWBFxN633SALPMGYaWZvKe9j1pRZJpauvmxENSp/EA==",
+      "requires": {
+        "domelementtype": "^2.3.0",
+        "domhandler": "^5.0.2",
+        "domutils": "^3.0.1",
+        "entities": "^4.3.0"
+      }
+    },
     "http-deceiver": {
       "version": "1.2.7",
       "resolved": "https://registry.npmjs.org/http-deceiver/-/http-deceiver-1.2.7.tgz",
@@ -11341,6 +12082,11 @@
         "loose-envify": "^1.0.0"
       }
     },
+    "ip-anonymize": {
+      "version": "0.1.0",
+      "resolved": "https://registry.npmjs.org/ip-anonymize/-/ip-anonymize-0.1.0.tgz",
+      "integrity": "sha512-cZJu+N5JKKFGMK0eEQWNaQMn2EhCysciVM6eotCJwfqotj16BTfVchKsJCH6mQAT9N0GC7oWRcsZ6Lb8dDiwTA=="
+    },
     "ipaddr.js": {
       "version": "1.9.1",
       "resolved": "https://registry.npmjs.org/ipaddr.js/-/ipaddr.js-1.9.1.tgz",
@@ -11519,6 +12265,65 @@
       "integrity": "sha512-dcS1ul+9tmeD95T+x28/ehLgd9mENa3LsvDTtzm3vyBEO7RPptvAD+t44WVXaUjTBRcrpFeFlC8WCruUR456hw==",
       "dev": true
     },
+    "lean4": {
+      "version": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?a51db90",
+      "integrity": "sha512-eKDMAR/1LvozI+Zhw4smMerwhYi2aZR1Yf0v5jbxu3g5z4YMMhYJpYhbtVhf4Za0boSsol2+z2dxc8fBI/1LOg==",
+      "requires": {
+        "@esm-bundle/react": "^17.0.2-fix.1",
+        "@esm-bundle/react-dom": "^17.0.2-fix.0",
+        "@leanprover/infoview": "^0.2.0",
+        "@leanprover/infoview-api": "^0.1.0",
+        "axios": "^0.24.0",
+        "cheerio": "^1.0.0-rc.10",
+        "mobx": "5.15.7",
+        "semver": "=7.3.5",
+        "vscode-languageclient": "=8.0.2"
+      },
+      "dependencies": {
+        "mobx": {
+          "version": "5.15.7",
+          "resolved": "https://registry.npmjs.org/mobx/-/mobx-5.15.7.tgz",
+          "integrity": "sha512-wyM3FghTkhmC+hQjyPGGFdpehrcX1KOXsDuERhfK2YbJemkUhEB+6wzEN639T21onxlfYBmriA1PFnvxTUhcKw=="
+        },
+        "semver": {
+          "version": "7.3.5",
+          "resolved": "https://registry.npmjs.org/semver/-/semver-7.3.5.tgz",
+          "integrity": "sha512-PoeGJYh8HK4BTO/a9Tf6ZG3veo/A7ZVsYrSA6J8ny9nb3B1VrpkuN+z9OE5wfE5p6H4LchYZsegiQgbJD94ZFQ==",
+          "requires": {
+            "lru-cache": "^6.0.0"
+          }
+        }
+      }
+    },
+    "lean4web": {
+      "version": "git+ssh://git@github.com/hhu-adam/lean4web.git#3be4ce778bbd7507876d5414dc99f5d44a60a274",
+      "from": "lean4web@git+https://github.com/hhu-adam/lean4web.git",
+      "requires": {
+        "@fontsource/roboto": "^4.5.8",
+        "@fontsource/roboto-mono": "^4.5.8",
+        "@fortawesome/fontawesome-svg-core": "^6.2.0",
+        "@fortawesome/free-solid-svg-icons": "^6.2.0",
+        "@fortawesome/react-fontawesome": "^0.2.0",
+        "@leanprover/infoview": "git+https://github.com/abentkamp/infoview-npm.git",
+        "express": "^4.18.2",
+        "file-saver": "^2.0.5",
+        "ip-anonymize": "^0.1.0",
+        "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?a51db90",
+        "mobx": "^6.6.2",
+        "monaco-editor": "^0.34.1",
+        "monaco-editor-textmate": "^4.0.0",
+        "monaco-languageclient": "^4.0.1",
+        "monaco-textmate": "^3.0.1",
+        "onigasm": "^2.2.5",
+        "path-browserify": "^1.0.1",
+        "react": "^18.2.0",
+        "react-dom": "^18.2.0",
+        "react-split": "^2.0.14",
+        "stream-http": "^3.2.0",
+        "vscode-ws-jsonrpc": "^2.0.0",
+        "ws": "^8.9.0"
+      }
+    },
     "lines-and-columns": {
       "version": "1.2.4",
       "resolved": "https://registry.npmjs.org/lines-and-columns/-/lines-and-columns-1.2.4.tgz",
@@ -11570,7 +12375,6 @@
       "version": "6.0.0",
       "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz",
       "integrity": "sha512-Jo6dJ04CmSjuznwJSS3pUeWmd/H0ffTlkXXgwZi+eq1UCmqQwCh+eLsYOYCwY991i2Fah4h1BEMCx4qThGbsiA==",
-      "dev": true,
       "requires": {
         "yallist": "^4.0.0"
       }
@@ -11590,6 +12394,11 @@
         "semver": "^6.0.0"
       }
     },
+    "marked": {
+      "version": "4.2.3",
+      "resolved": "https://registry.npmjs.org/marked/-/marked-4.2.3.tgz",
+      "integrity": "sha512-slWRdJkbTZ+PjkyJnE30Uid64eHwbwa1Q25INCAYfZlK4o6ylagBy/Le9eWntqJFoFT93ikUKMv47GZ4gTwHkw=="
+    },
     "mathjax-full": {
       "version": "3.2.2",
       "resolved": "https://registry.npmjs.org/mathjax-full/-/mathjax-full-3.2.2.tgz",
@@ -11942,7 +12751,6 @@
       "version": "3.1.2",
       "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-3.1.2.tgz",
       "integrity": "sha512-J7p63hRiAjw1NDEww1W7i37+ByIrOWO5XQQAzZ3VOcL0PNybwpfmV/N05zFAzwQ9USyEcX6t3UO+K5aqBQOIHw==",
-      "dev": true,
       "requires": {
         "brace-expansion": "^1.1.7"
       }
@@ -11952,6 +12760,40 @@
       "resolved": "https://registry.npmjs.org/mj-context-menu/-/mj-context-menu-0.6.1.tgz",
       "integrity": "sha512-7NO5s6n10TIV96d4g2uDpG7ZDpIhMh0QNfGdJw/W47JswFcosz457wqz/b5sAKvl12sxINGFCn80NZHKwxQEXA=="
     },
+    "mobx": {
+      "version": "6.7.0",
+      "resolved": "https://registry.npmjs.org/mobx/-/mobx-6.7.0.tgz",
+      "integrity": "sha512-1kBLBdSNG2bA522HQdbsTvwAwYf9hq9FWxmlhX7wTsJUAI54907J+ozfGW+LoYUo06vjit748g6QH1AAGLNebw=="
+    },
+    "monaco-editor": {
+      "version": "0.34.1",
+      "resolved": "https://registry.npmjs.org/monaco-editor/-/monaco-editor-0.34.1.tgz",
+      "integrity": "sha512-FKc80TyiMaruhJKKPz5SpJPIjL+dflGvz4CpuThaPMc94AyN7SeC9HQ8hrvaxX7EyHdJcUY5i4D0gNyJj1vSZQ=="
+    },
+    "monaco-editor-textmate": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/monaco-editor-textmate/-/monaco-editor-textmate-4.0.0.tgz",
+      "integrity": "sha512-Clwup5LJzVfwURQrS+odSEC5/hZBEG36pQnvBKt4OtBndF8r2xLeXUZcK/AqEBK2u0Npy7frFp9hG7m66Ol9hA==",
+      "requires": {}
+    },
+    "monaco-languageclient": {
+      "version": "4.0.1",
+      "resolved": "https://registry.npmjs.org/monaco-languageclient/-/monaco-languageclient-4.0.1.tgz",
+      "integrity": "sha512-mUIq/7gQM/8CyOBVGv0thLRAR80vk49Ur0ROJveoh6R0/uwaUoyri+5OBslxsa5BICftLTsC8/Y+at6/iW50Ww==",
+      "requires": {
+        "vscode": "npm:@codingame/monaco-vscode-api@1.69.12",
+        "vscode-jsonrpc": "8.0.2",
+        "vscode-languageclient": "8.0.2"
+      }
+    },
+    "monaco-textmate": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/monaco-textmate/-/monaco-textmate-3.0.1.tgz",
+      "integrity": "sha512-ZxxY3OsqUczYP1sGqo97tu+CJmMBwuSW+dL0WEBdDhOZ5G1zntw72hvBc68ZQAirosWvbDKgN1dL5k173QtFww==",
+      "requires": {
+        "fast-plist": "^0.1.2"
+      }
+    },
     "mri": {
       "version": "1.2.0",
       "resolved": "https://registry.npmjs.org/mri/-/mri-1.2.0.tgz",
@@ -12060,6 +12902,14 @@
         "path-key": "^3.0.0"
       }
     },
+    "nth-check": {
+      "version": "2.1.1",
+      "resolved": "https://registry.npmjs.org/nth-check/-/nth-check-2.1.1.tgz",
+      "integrity": "sha512-lqjrjmaOoAnWfMmBPL+XNnynZh2+swxiX3WUE0s4yEHI6m+AwrK2UZOimIRl3X/4QctVqS8AiZjFqyOGrMXb/w==",
+      "requires": {
+        "boolbase": "^1.0.0"
+      }
+    },
     "object-assign": {
       "version": "4.1.1",
       "resolved": "https://registry.npmjs.org/object-assign/-/object-assign-4.1.1.tgz",
@@ -12126,6 +12976,29 @@
         "mimic-fn": "^2.1.0"
       }
     },
+    "onigasm": {
+      "version": "2.2.5",
+      "resolved": "https://registry.npmjs.org/onigasm/-/onigasm-2.2.5.tgz",
+      "integrity": "sha512-F+th54mPc0l1lp1ZcFMyL/jTs2Tlq4SqIHKIXGZOR/VkHkF9A7Fr5rRr5+ZG/lWeRsyrClLYRq7s/yFQ/XhWCA==",
+      "requires": {
+        "lru-cache": "^5.1.1"
+      },
+      "dependencies": {
+        "lru-cache": {
+          "version": "5.1.1",
+          "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-5.1.1.tgz",
+          "integrity": "sha512-KpNARQA3Iwv+jTA0utUVVbrh+Jlrr1Fv0e56GGzAFOXN7dk/FviaDW8LHmK52DlcH4WP2n6gI8vN1aesBFgo9w==",
+          "requires": {
+            "yallist": "^3.0.2"
+          }
+        },
+        "yallist": {
+          "version": "3.1.1",
+          "resolved": "https://registry.npmjs.org/yallist/-/yallist-3.1.1.tgz",
+          "integrity": "sha512-a4UGQaWPH59mOXUYnAG2ewncQS4i4F43Tv3JoAM+s2VDAmS9NsK8GpDMLrCHPksFT7h3K6TOoUNn2pb7RoXx4g=="
+        }
+      }
+    },
     "open": {
       "version": "8.4.0",
       "resolved": "https://registry.npmjs.org/open/-/open-8.4.0.tgz",
@@ -12194,11 +13067,33 @@
         "lines-and-columns": "^1.1.6"
       }
     },
+    "parse5": {
+      "version": "7.1.2",
+      "resolved": "https://registry.npmjs.org/parse5/-/parse5-7.1.2.tgz",
+      "integrity": "sha512-Czj1WaSVpaoj0wbhMzLmWD69anp2WH7FXMB9n1Sy8/ZFF9jolSQVMu1Ij5WIyGmcBmhk7EOndpO4mIpihVqAXw==",
+      "requires": {
+        "entities": "^4.4.0"
+      }
+    },
+    "parse5-htmlparser2-tree-adapter": {
+      "version": "7.0.0",
+      "resolved": "https://registry.npmjs.org/parse5-htmlparser2-tree-adapter/-/parse5-htmlparser2-tree-adapter-7.0.0.tgz",
+      "integrity": "sha512-B77tOZrqqfUfnVcOrUvfdLbz4pu4RopLD/4vmu3HUPswwTA8OH0EMW9BlWR2B0RCoiZRAHEUu7IxeP1Pd1UU+g==",
+      "requires": {
+        "domhandler": "^5.0.2",
+        "parse5": "^7.0.0"
+      }
+    },
     "parseurl": {
       "version": "1.3.3",
       "resolved": "https://registry.npmjs.org/parseurl/-/parseurl-1.3.3.tgz",
       "integrity": "sha512-CiyeOxFT/JZyN5m0z9PfXw4SCBJ6Sygz1Dpl0wqjlhDEGGBP1GnsUVEL0p63hoG1fcj3fHynXi9NYO4nWOL+qQ=="
     },
+    "path-browserify": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/path-browserify/-/path-browserify-1.0.1.tgz",
+      "integrity": "sha512-b7uo2UCUOYZcnF/3ID0lulOJi/bafxa1xPe7ZPsammBSpjSWQkjNxlt635YGS2MiR9GjvuXCtz2emr3jbsz98g=="
+    },
     "path-exists": {
       "version": "4.0.0",
       "resolved": "https://registry.npmjs.org/path-exists/-/path-exists-4.0.0.tgz",
@@ -12488,6 +13383,11 @@
         "scheduler": "^0.23.0"
       }
     },
+    "react-fast-compare": {
+      "version": "3.2.0",
+      "resolved": "https://registry.npmjs.org/react-fast-compare/-/react-fast-compare-3.2.0.tgz",
+      "integrity": "sha512-rtGImPZ0YyLrscKI9xTpV8psd6I8VAtjKCzQDlzyDvqJA8XOW78TXYQwNRNd8g8JZnDu8q9Fu/1v4HPAVwVdHA=="
+    },
     "react-is": {
       "version": "18.2.0",
       "resolved": "https://registry.npmjs.org/react-is/-/react-is-18.2.0.tgz",
@@ -12521,6 +13421,15 @@
       "integrity": "sha512-wViHqhAd8OHeLS/IRMJjTSDHF3U9eWi62F/MledQGPdJGDhodXJ9PBLNGr6WWL7qlH12Mt3TyTpbS+hGXMjCzQ==",
       "dev": true
     },
+    "react-split": {
+      "version": "2.0.14",
+      "resolved": "https://registry.npmjs.org/react-split/-/react-split-2.0.14.tgz",
+      "integrity": "sha512-bKWydgMgaKTg/2JGQnaJPg51T6dmumTWZppFgEbbY0Fbme0F5TuatAScCLaqommbGQQf/ZT1zaejuPDriscISA==",
+      "requires": {
+        "prop-types": "^15.5.7",
+        "split.js": "^1.6.0"
+      }
+    },
     "react-transition-group": {
       "version": "4.4.5",
       "resolved": "https://registry.npmjs.org/react-transition-group/-/react-transition-group-4.4.5.tgz",
@@ -13100,6 +14009,11 @@
         }
       }
     },
+    "split.js": {
+      "version": "1.6.5",
+      "resolved": "https://registry.npmjs.org/split.js/-/split.js-1.6.5.tgz",
+      "integrity": "sha512-mPTnGCiS/RiuTNsVhCm9De9cCAUsrNFFviRbADdKiiV+Kk8HKp/0fWu7Kr8pi3/yBmsqLFHuXGT9UUZ+CNLwFw=="
+    },
     "stackframe": {
       "version": "1.3.4",
       "resolved": "https://registry.npmjs.org/stackframe/-/stackframe-1.3.4.tgz",
@@ -13111,11 +14025,33 @@
       "resolved": "https://registry.npmjs.org/statuses/-/statuses-2.0.1.tgz",
       "integrity": "sha512-RwNA9Z/7PrK06rYLIzFMlaF+l73iwpzsqRIFgbMLbTcLD6cOao82TaWefPXQvB2fOC4AjuYSEndS7N/mTCbkdQ=="
     },
+    "stream-http": {
+      "version": "3.2.0",
+      "resolved": "https://registry.npmjs.org/stream-http/-/stream-http-3.2.0.tgz",
+      "integrity": "sha512-Oq1bLqisTyK3TSCXpPbT4sdeYNdmyZJv1LxpEm2vu1ZhK89kSE5YXwZc3cWk0MagGaKriBh9mCFbVGtO+vY29A==",
+      "requires": {
+        "builtin-status-codes": "^3.0.0",
+        "inherits": "^2.0.4",
+        "readable-stream": "^3.6.0",
+        "xtend": "^4.0.2"
+      },
+      "dependencies": {
+        "readable-stream": {
+          "version": "3.6.0",
+          "resolved": "https://registry.npmjs.org/readable-stream/-/readable-stream-3.6.0.tgz",
+          "integrity": "sha512-BViHy7LKeTz4oNnkcLJ+lVSL6vpiFeX6/d3oSH8zCW7UxP2onchk+vTGB143xuFjHS3deTgkKoXXymXqymiIdA==",
+          "requires": {
+            "inherits": "^2.0.3",
+            "string_decoder": "^1.1.1",
+            "util-deprecate": "^1.0.1"
+          }
+        }
+      }
+    },
     "string_decoder": {
       "version": "1.3.0",
       "resolved": "https://registry.npmjs.org/string_decoder/-/string_decoder-1.3.0.tgz",
       "integrity": "sha512-hkRX8U1WjJFd8LsDJ2yQ/wWWxaopEsABU1XfkM8A+j0+85JAGppt16cr1Whg6KIbb4okU6Mql6BOj+uup/wKeA==",
-      "dev": true,
       "requires": {
         "safe-buffer": "~5.2.0"
       }
@@ -13170,6 +14106,11 @@
       "integrity": "sha512-ot0WnXS9fgdkgIcePe6RHNk1WA8+muPa6cSjeR3V8K27q9BB1rTE3R1p7Hv0z1ZyAc8s6Vvv8DIyWf681MAt0w==",
       "devOptional": true
     },
+    "tachyons": {
+      "version": "4.12.0",
+      "resolved": "https://registry.npmjs.org/tachyons/-/tachyons-4.12.0.tgz",
+      "integrity": "sha512-2nA2IrYFy3raCM9fxJ2KODRGHVSZNTW3BR0YnlGsLUf1DA3pk3YfWZ/DdfbnZK6zLZS+jUenlUGJsKcA5fUiZg=="
+    },
     "tapable": {
       "version": "2.2.1",
       "resolved": "https://registry.npmjs.org/tapable/-/tapable-2.2.1.tgz",
@@ -13473,8 +14414,7 @@
     "util-deprecate": {
       "version": "1.0.2",
       "resolved": "https://registry.npmjs.org/util-deprecate/-/util-deprecate-1.0.2.tgz",
-      "integrity": "sha512-EPD5q1uXyFxJpCrLnCc1nHnq3gOa6DZBocAIiI2TaSCA7VCJ1UJDMagCzIkXNsUYfD1daK//LTEQ8xiIbrHtcw==",
-      "dev": true
+      "integrity": "sha512-EPD5q1uXyFxJpCrLnCc1nHnq3gOa6DZBocAIiI2TaSCA7VCJ1UJDMagCzIkXNsUYfD1daK//LTEQ8xiIbrHtcw=="
     },
     "utils-merge": {
       "version": "1.0.1",
@@ -13530,11 +14470,65 @@
         "unist-util-stringify-position": "^3.0.0"
       }
     },
+    "vscode": {
+      "version": "npm:@codingame/monaco-vscode-api@1.69.12",
+      "resolved": "https://registry.npmjs.org/@codingame/monaco-vscode-api/-/monaco-vscode-api-1.69.12.tgz",
+      "integrity": "sha512-ES1xRnU232t82tcdM2ImikkjGfAMgJtrF0XkLa4poEnvcUH0SFqUhYvcqk5CFggQWh16jqxifVvozcu0/mbH7A==",
+      "requires": {
+        "monaco-editor": "^0.34.0"
+      }
+    },
     "vscode-jsonrpc": {
       "version": "8.0.2",
       "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-8.0.2.tgz",
       "integrity": "sha512-RY7HwI/ydoC1Wwg4gJ3y6LpU9FJRZAUnTYMXthqhFXXu77ErDd/xkREpGuk4MyYkk4a+XDWAMqe0S3KkelYQEQ=="
     },
+    "vscode-languageclient": {
+      "version": "8.0.2",
+      "resolved": "https://registry.npmjs.org/vscode-languageclient/-/vscode-languageclient-8.0.2.tgz",
+      "integrity": "sha512-lHlthJtphG9gibGb/y72CKqQUxwPsMXijJVpHEC2bvbFqxmkj9LwQ3aGU9dwjBLqsX1S4KjShYppLvg1UJDF/Q==",
+      "requires": {
+        "minimatch": "^3.0.4",
+        "semver": "^7.3.5",
+        "vscode-languageserver-protocol": "3.17.2"
+      },
+      "dependencies": {
+        "semver": {
+          "version": "7.3.8",
+          "resolved": "https://registry.npmjs.org/semver/-/semver-7.3.8.tgz",
+          "integrity": "sha512-NB1ctGL5rlHrPJtFDVIVzTyQylMLu9N9VICA6HSFJo8MCGVTMW6gfpicwKmmK/dAjTOrqu5l63JJOpDSrAis3A==",
+          "requires": {
+            "lru-cache": "^6.0.0"
+          }
+        }
+      }
+    },
+    "vscode-languageserver-protocol": {
+      "version": "3.17.2",
+      "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.17.2.tgz",
+      "integrity": "sha512-8kYisQ3z/SQ2kyjlNeQxbkkTNmVFoQCqkmGrzLH6A9ecPlgTbp3wDTnUNqaUxYr4vlAcloxx8zwy7G5WdguYNg==",
+      "requires": {
+        "vscode-jsonrpc": "8.0.2",
+        "vscode-languageserver-types": "3.17.2"
+      }
+    },
+    "vscode-languageserver-types": {
+      "version": "3.17.2",
+      "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.17.2.tgz",
+      "integrity": "sha512-zHhCWatviizPIq9B7Vh9uvrH6x3sK8itC84HkamnBWoDFJtzBf7SWlpLCZUit72b3os45h6RWQNC9xHRDF8dRA=="
+    },
+    "vscode-oniguruma": {
+      "version": "1.6.2",
+      "resolved": "https://registry.npmjs.org/vscode-oniguruma/-/vscode-oniguruma-1.6.2.tgz",
+      "integrity": "sha512-KH8+KKov5eS/9WhofZR8M8dMHWN2gTxjMsG4jd04YhpbPR91fUj7rYQ2/XjeHCJWbg7X++ApRIU9NUwM2vTvLA==",
+      "peer": true
+    },
+    "vscode-textmate": {
+      "version": "7.0.3",
+      "resolved": "https://registry.npmjs.org/vscode-textmate/-/vscode-textmate-7.0.3.tgz",
+      "integrity": "sha512-OkE/mYm1h5ZX9IEKeKR/2zKDt2SzYyIfTEOVFX4QhA+B3BPROvNEmDDXvBThz3qknKO3Cy/VVb8/sx1UlqP/Xw==",
+      "peer": true
+    },
     "vscode-ws-jsonrpc": {
       "version": "2.0.0",
       "resolved": "https://registry.npmjs.org/vscode-ws-jsonrpc/-/vscode-ws-jsonrpc-2.0.0.tgz",
@@ -13862,11 +14856,15 @@
       "resolved": "https://registry.npmjs.org/xmldom-sre/-/xmldom-sre-0.1.31.tgz",
       "integrity": "sha512-f9s+fUkX04BxQf+7mMWAp5zk61pciie+fFLC9hX9UVvCeJQfNHRHXpeo5MPcR0EUf57PYLdt+ZO4f3Ipk2oZUw=="
     },
+    "xtend": {
+      "version": "4.0.2",
+      "resolved": "https://registry.npmjs.org/xtend/-/xtend-4.0.2.tgz",
+      "integrity": "sha512-LKYU1iAXJXUgAXn9URjiu+MWhyUXHsvfp7mcuYm9dSUKK0/CjtrUwFAxD82/mCWbtLsGjFIad0wIsod4zrTAEQ=="
+    },
     "yallist": {
       "version": "4.0.0",
       "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz",
-      "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A==",
-      "dev": true
+      "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A=="
     },
     "yaml": {
       "version": "1.10.2",
diff --git a/package.json b/package.json
index 3ec2c02..4a4980e 100644
--- a/package.json
+++ b/package.json
@@ -10,6 +10,8 @@
     "@mui/material": "^5.10.9",
     "better-react-mathjax": "^2.0.2",
     "express": "^4.18.2",
+    "lean4web": "git+https://github.com/hhu-adam/lean4web.git",
+    "path-browserify": "^1.0.1",
     "react": "^18.2.0",
     "react-dom": "^18.2.0",
     "react-markdown": "^8.0.3",
diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index 1ad00e9..054d62a 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -269,7 +269,7 @@ section Initialization
         if path.fileName != "lakefile.lean" && (← System.FilePath.pathExists lakePath) then
           let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut
           srcSearchPath ← initSrcSearchPath (← getBuildDir) pkgSearchPath
-      let env ← importModules [{module := `Init}, {module := `Lib}] opts 0
+      let env ← importModules [{module := `Init}] opts 0
       pure (env, msgLog)
     catch e =>  -- should be from `lake print-paths`
       let msgs := MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }
diff --git a/tsconfig.json b/tsconfig.json
index b55636b..8952160 100644
--- a/tsconfig.json
+++ b/tsconfig.json
@@ -1,10 +1,14 @@
 {
   "compilerOptions": {
     "outDir": "./client/dist/",
-    "module": "es6",
+    "module": "esnext",
     "target": "es5",
     "allowJs": true,
+    "resolveJsonModule": true,
+    "esModuleInterop": true,
     "moduleResolution": "node",
     "jsx": "react",
+    "downlevelIteration": true,
+    "experimentalDecorators": true
   }
-}
\ No newline at end of file
+}
diff --git a/webpack.config.js b/webpack.config.js
index 244e4bd..2d8864d 100644
--- a/webpack.config.js
+++ b/webpack.config.js
@@ -1,4 +1,5 @@
 const path = require("path");
+const webpack = require('webpack');
 const ReactRefreshWebpackPlugin = require('@pmmmwh/react-refresh-webpack-plugin');
 const WebpackShellPluginNext = require('webpack-shell-plugin-next');
 
@@ -31,8 +32,12 @@ module.exports = env => {
         },
         {
           test: /\.tsx?$/,
-          use: 'ts-loader',
-          exclude: /node_modules/,
+          use: [{
+            loader: 'ts-loader',
+            options: { allowTsInNodeModules: true }
+          }],
+          exclude: /node_modules(?!\/(lean4web|lean4))/,
+          // Allow .ts imports from node_modules/lean4web and node_modules/lean4
         },
         {
           test: /\.css$/,
@@ -40,7 +45,13 @@ module.exports = env => {
         }
       ]
     },
-    resolve: { extensions: ["*", ".js", ".jsx", ".tsx", ".ts"] },
+    resolve: {
+      extensions: ["*", ".js", ".jsx", ".tsx", ".ts"],
+      fallback: {
+        "http": require.resolve("stream-http") ,
+        "path": require.resolve("path-browserify")
+      },
+    },
     output: {
       path: path.resolve(__dirname, "client/dist/"),
       filename: "bundle.js",
@@ -60,14 +71,27 @@ module.exports = env => {
     plugins: [
       !isDevelopment && new WebpackShellPluginNext({
         onBuildEnd:{
-          // It's hard to set up webpack to copy the index.html correctly,
-          // so we copy it explicitly after every build:
-          scripts: ['cp client/public/index.html client/dist/'],
+          scripts: [
+            // It's hard to set up webpack to copy the index.html correctly,
+            // so we copy it explicitly after every build:
+            'cp client/public/index.html client/dist/',
+            // Similarly, I haven't been able to load `onigasm.wasm` properly:
+            'cp client/public/onigasm.wasm client/dist/',],
           blocking: false,
           parallel: true
         }
       }),
-      isDevelopment && new ReactRefreshWebpackPlugin()
+      isDevelopment && new ReactRefreshWebpackPlugin(),
+      new webpack.ContextReplacementPlugin(
+        /\/@leanprover\/infoview\//,
+        (data) => {
+          // Webpack is not happy about the dynamically loaded widget code in the function
+          // `dynamicallyLoadComponent` in `infoview/userWidget.tsx`. If we want to support
+          // dynamically loaded widget code, we need to make sure that the files are available.
+          delete data.dependencies[0].critical;
+          return data;
+        },
+      ),
     ].filter(Boolean),
   };
 }