use LeanClient

client/src/App.tsx

@@ -2,6 +2,7 @@ import * as React from 'react';
 import { useState, useEffect } from 'react';
 import { MathJaxContext } from "better-react-mathjax";
 import * as rpc from 'vscode-ws-jsonrpc';
+import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 
 import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
@@ -14,6 +15,12 @@ import Welcome from './components/Welcome';
 import Level from './components/Level';
 import GoodBye from './components/GoodBye';
 import useWebSocket from 'react-use-websocket';
+import { LeanClient } from 'lean4web/client/src/editor/leanclient';
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
+
+const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/'
+
+monacoSetup()
 
 function App() {
   const [title, setTitle] = useState("")
@@ -22,22 +29,14 @@ function App() {
   const [nbLevels, setNbLevels] = useState(0)
   const [curLevel, setCurLevel] = useState(0)
   const [finished, setFinished] = useState(false)
-  const [rpcConnection, setRpcConnection] = useState<null|rpc.MessageConnection>(null)
+  const [leanClient, setLeanClient] = useState<null|LeanClient>(null)
 
-  const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/'
+  useEffect(() => {
+    const uri = monaco.Uri.parse('file:///LeanProject/Level1.lean')
+    const leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
+    setLeanClient(leanClient)
+  }, [])
 
-  useWebSocket(socketUrl, {
-    onOpen: function (ev) {
-      const logger = new rpc.ConsoleLogger();
-      const socket = rpc.toSocket(ev.target as WebSocket);
-      let rpcConnection = rpc.createWebSocketConnection(socket, logger)
-      setRpcConnection(rpcConnection);
-      rpcConnection.listen();
-    },
-    onMessage: (msg) => {
-      console.log(msg)
-    }
-  })
 
   const mathJaxConfig = {
     loader: {
@@ -59,9 +58,9 @@ function App() {
   if (finished) {
     mainComponent = <GoodBye message={conclusion} />
   } else if (curLevel > 0) {
-    mainComponent = <Level rpcConnection={rpcConnection} nbLevels={nbLevels} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
+    mainComponent = <Level leanClient={leanClient} nbLevels={nbLevels} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
   } else {
-    mainComponent = <Welcome rpcConnection={rpcConnection} setNbLevels={setNbLevels} setTitle={setTitle} startGame={startGame} setConclusion={setConclusion}/>
+    mainComponent = <Welcome leanClient={leanClient} setNbLevels={setNbLevels} setTitle={setTitle} startGame={startGame} setConclusion={setConclusion}/>
   }
 
   return (

client/src/components/Level.tsx

@@ -1,5 +1,5 @@
 import * as React from 'react';
-import { useEffect, useState } from 'react';
+import { useEffect, useState, useRef } from 'react';
 import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
@@ -11,11 +11,11 @@ import LeftPanel from './LeftPanel';
 import InputZone from './InputZone';
 import Message from './Message';
 import TacticState from './TacticState';
-import * as rpc from 'vscode-ws-jsonrpc';
+import { LeanClient } from 'lean4web/client/src/editor/leanclient';
-import Editor from 'lean4web/client/src/Editor'
+import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 
 interface LevelProps {
-  rpcConnection: null|rpc.MessageConnection;
+  leanClient: null|LeanClient;
   nbLevels: any;
   level: any;
   setCurLevel: any;
@@ -23,7 +23,7 @@ interface LevelProps {
   setFinished: any
 }
 
-function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, setFinished }: LevelProps) {
+function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFinished }: LevelProps) {
   const [index, setIndex] = useState(level) // Level number
   const [tacticDocs, setTacticDocs] = useState([])
   const [lemmaDocs, setLemmaDocs] = useState([])
@@ -32,6 +32,7 @@ function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, set
   const [history, setHistory] = useState([])
   const [lastTactic, setLastTactic] = useState("")
   const [errors, setErrors] = useState([])
+  const codeviewRef = useRef<HTMLDivElement>(null)
 
   const [message, setMessage] = useState("")
   const [messageOpen, setMessageOpen] = useState(false)
@@ -53,26 +54,53 @@ function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, set
 
   // The next function will be called when the level changes
   useEffect(() => {
-    if (rpcConnection) {
+    const uri = monaco.Uri.parse('file:///LeanProject/Level1.lean')
-      rpcConnection.sendRequest("loadLevel", {number: level}).then((res) => {
+    const model = monaco.editor.createModel('', 'lean4', uri)
-        setLevelTitle("Level " + res["index"] + ": " + res["title"])
+    const editor = monaco.editor.create(codeviewRef.current!, {
-        setIndex(parseInt(res["index"]))
+      model,
-        setTacticDocs(res["tactics"])
+      glyphMargin: true,
-        setLemmaDocs(res["lemmas"])
+      lightbulb: {
-        processResponse(res)
+        enabled: true
-      });
+      },
-    }
+      unicodeHighlight: {
-  }, [level, rpcConnection])
+          ambiguousCharacters: false,
+      },
+      automaticLayout: true,
+      minimap: {
+        enabled: false
+      },
+      lineNumbersMinChars: 3,
+      'semanticHighlighting.enabled': true,
+      theme: 'vs-code-theme-converted'
+    })
+    // setEditor(editor)
+    // new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+
+
+    // const infoProvider = new InfoProvider(leanClient)
+    // const div: HTMLElement = infoviewRef.current!
+    // const infoviewApi = renderInfoview(infoProvider.getApi(), div)
+    // setInfoProvider(infoProvider)
+    // setInfoviewApi(infoviewApi)
+
+    leanClient.sendRequest("loadLevel", {number: level}).then((res) => {
+      setLevelTitle("Level " + res["index"] + ": " + res["title"])
+      setIndex(parseInt(res["index"]))
+      setTacticDocs(res["tactics"])
+      setLemmaDocs(res["lemmas"])
+      processResponse(res)
+    });
+  }, [level, leanClient])
 
   function sendTactic(input) {
-    rpcConnection.sendRequest("runTactic", {tactic: input}).then(processResponse);
+    leanClient.sendRequest("runTactic", {tactic: input}).then(processResponse);
     setLastTactic(input);
     setHistory(history.concat([input]));
   }
 
   function undo() {
     if (errors.length === 0) {
-      rpcConnection.sendRequest('undo').then(processResponse);
+      leanClient.sendRequest('undo', {}).then(processResponse);
     }
     if (history.length > 1) {
       setLastTactic(history[history.length - 1]);
@@ -104,8 +132,7 @@ function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, set
         <LeftPanel spells={tacticDocs} inventory={lemmaDocs} />
       </Grid>
       <Grid xs={4}>
-        <Editor setRestart={() => {}}
+        <div ref={codeviewRef} className="codeview" style={{height: "20em"}}></div>
-          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} />

client/src/components/Welcome.tsx

@@ -9,9 +9,10 @@ import '@fontsource/roboto/700.css';
 import * as rpc from 'vscode-ws-jsonrpc';
 
 import { Box, Typography, Button, CircularProgress, Grid } from '@mui/material';
+import { LeanClient } from 'lean4web/client/src/editor/leanclient';
 
 interface WelcomeProps {
-  rpcConnection: null|rpc.MessageConnection;
+  leanClient: null|LeanClient;
   setNbLevels: any;
   setTitle: any;
   startGame: any;
@@ -24,29 +25,25 @@ type infoResultType = {
   conclusion: string
 }
 
-const initializeRequestType = new rpc.RequestType0<any, void>("initialize")
+function Welcome({ leanClient, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) {
-const initializedNotificationType = new rpc.NotificationType0("initialized")
-const infoRequestType = new rpc.RequestType1<string, infoResultType, void>("info")
-
-function Welcome({ rpcConnection, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) {
 
   const [leanData, setLeanData] = useState<null|infoResultType>(null)
 
   useEffect(() => {
-    if (rpcConnection) { // Will run in the beginning as soon as RPC connection is established
+    if (!leanClient) return;
-      rpcConnection.sendRequest(initializeRequestType).then((res: any) => {
+
-        rpcConnection.onRequest("client/registerCapability", () => {})
+    const getInfo = async () => {
-        rpcConnection.sendNotification(initializedNotificationType)
+      await leanClient.start() // TODO: need a way to wait for start without restarting
-        rpcConnection.sendRequest(infoRequestType, "hello").then((res: infoResultType) =>{
+      leanClient.sendRequest("info", "hello").then((res: infoResultType) =>{
-          setLeanData(res)
+        setLeanData(res)
-          setNbLevels(res.nb_levels)
+        setNbLevels(res.nb_levels)
-          setTitle(res.title)
+        setTitle(res.title)
-          document.title = res.title
+        document.title = res.title
-          setConclusion(res.conclusion)
+        setConclusion(res.conclusion)
-        });
       });
     }
-  }, [rpcConnection, setLeanData, setNbLevels, setTitle, setConclusion])
+    getInfo()
+  }, [leanClient])
 
   let content
   if (leanData) {

package-lock.json

@@ -14,7 +14,7 @@
         "@mui/material": "^5.10.9",
         "better-react-mathjax": "^2.0.2",
         "express": "^4.18.2",
-        "lean4web": "git+https://github.com/hhu-adam/lean4web.git",
+        "lean4web": "github:hhu-adam/lean4web",
         "path-browserify": "^1.0.1",
         "react": "^18.2.0",
         "react-dom": "^18.2.0",
@@ -5005,7 +5005,7 @@
     },
     "node_modules/lean4web": {
       "version": "0.1.0",
-      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#3be4ce778bbd7507876d5414dc99f5d44a60a274",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#465694da60e2afbf7d188b41af173998ae75d915",
       "dependencies": {
         "@fontsource/roboto": "^4.5.8",
         "@fontsource/roboto-mono": "^4.5.8",
@@ -12296,7 +12296,7 @@
       }
     },
     "lean4web": {
-      "version": "git+ssh://git@github.com/hhu-adam/lean4web.git#3be4ce778bbd7507876d5414dc99f5d44a60a274",
+      "version": "git+ssh://git@github.com/hhu-adam/lean4web.git#465694da60e2afbf7d188b41af173998ae75d915",
       "from": "lean4web@git+https://github.com/hhu-adam/lean4web.git",
       "requires": {
         "@fontsource/roboto": "^4.5.8",

package.json

@@ -10,7 +10,7 @@
     "@mui/material": "^5.10.9",
     "better-react-mathjax": "^2.0.2",
     "express": "^4.18.2",
-    "lean4web": "git+https://github.com/hhu-adam/lean4web.git",
+    "lean4web": "github:hhu-adam/lean4web",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",
     "react-dom": "^18.2.0",