vite

leanprover-community · Oct 21, 2023 · 60ee990 · 60ee990
1 parent 3b07760
commit 60ee990
Show file tree

Hide file tree

Showing 14 changed files with 741 additions and 31 deletions.
diff --git a/client/public/index.production.min.js b/client/public/index.production.min.js
diff --git a/client/public/loader.production.min.js b/client/public/loader.production.min.js
diff --git a/client/public/react-dom.production.min.js b/client/public/react-dom.production.min.js
diff --git a/client/public/react-jsx-runtime.production.min.js b/client/public/react-jsx-runtime.production.min.js
diff --git a/client/public/react-popper.production.min.js b/client/public/react-popper.production.min.js
diff --git a/client/public/react.production.min.js b/client/public/react.production.min.js
diff --git a/client/src/App.tsx b/client/src/App.tsx
@@ -123,7 +123,7 @@ const App: React.FC = () => {
   return (
     <div className={`app ${theme}-theme`}>
       <div className='nav'>
-        <Logo className='logo' />
+        {/* <Logo className='logo' /> */}
         <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
           <Examples loadFromUrl={loadFromUrl} />
           <Settings closeNav={closeNav} theme={theme} setTheme={setTheme}/>

diff --git a/client/src/editor/abbreviation/AbbreviationProvider.ts b/client/src/editor/abbreviation/AbbreviationProvider.ts
@@ -28,7 +28,6 @@ export class AbbreviationProvider {
 		// );
 	}
 
-	@computed
 	private get symbolsByAbbreviation(): SymbolsByAbbreviation {
 		// There are only like 1000 symbols. Building an index is not required yet.
 		return {

diff --git a/client/src/editor/leanclient.ts b/client/src/editor/leanclient.ts
@@ -16,8 +16,7 @@ import {
   LanguageClientOptions,
   PublishDiagnosticsParams,
   CloseAction, ErrorAction,
-  RevealOutputChannelOn,
-  State
+  RevealOutputChannelOn
 } from 'monaco-languageclient'
 import * as ls from 'vscode-languageserver-protocol'
 import { toSocket, WebSocketMessageReader, WebSocketMessageWriter } from 'vscode-ws-jsonrpc'
@@ -349,16 +348,16 @@ export class LeanClient implements Disposable {
     try {
       this.client.onDidChangeState(async (s) => {
         // see https://github.com/microsoft/vscode-languageserver-node/issues/825
-        if (s.newState === State.Starting) {
+        if (s.newState === 3) {
           console.log('[LeanClient] starting')
-        } else if (s.newState === State.Running) {
+        } else if (s.newState === 2) {
           const end = Date.now()
           console.log(`[LeanClient] running, started in ${end - startTime} ms`)
           this.running = true // may have been auto restarted after it failed.
           if (!insideRestart) {
             this.restartedEmitter.fire(undefined)
           }
-        } else if (s.newState === State.Stopped) {
+        } else if (s.newState === 1) {
           this.running = false
           console.log('[LeanClient] has stopped or it failed to start')
           if (!this.noPrompt) {

diff --git a/index.html b/index.html
@@ -0,0 +1,28 @@
+<!DOCTYPE html>
+<html>
+
+<head>
+  <meta charset="UTF-8" />
+  <title>Lean 4 Web</title>
+  <meta name="viewport" content="width=device-width, initial-scale=1.0">
+</head>
+
+<body>
+  <div id="root"></div>
+  <noscript>
+    <p>You need to enable JavaScript to use the lean4web editor, as it is a <a href="https://react.dev">React app</a>.</p>
+    <p>Contact details:</p>
+    <p>
+      <a href="https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/dr-alexander-bentkamp">Alexander Bentkamp</a>,&nbsp;
+      <a href="https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Jon Eugster</a><br />
+      Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
+      Universitätsstr. 1<br />
+      40225 Düsseldorf<br />
+      Germany<br />
+      +49 211 81-12173<br />
+    </p>
+  </noscript>
+  <script type="module" src="/client/src/index.tsx"></script>
+</body>
+
+</html>