From 7ae299870bfbbbbdea6901937f2cce8baad7c94d Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 24 Nov 2022 13:03:02 +0100 Subject: [PATCH] use LeanClient --- client/src/App.tsx | 31 +++++++-------- client/src/components/Level.tsx | 65 ++++++++++++++++++++++--------- client/src/components/Welcome.tsx | 33 +++++++--------- package-lock.json | 6 +-- package.json | 2 +- 5 files changed, 80 insertions(+), 57 deletions(-) diff --git a/client/src/App.tsx b/client/src/App.tsx index b6087ce..43ffbfc 100644 --- a/client/src/App.tsx +++ b/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) + const [leanClient, setLeanClient] = useState(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 = } else if (curLevel > 0) { - mainComponent = + mainComponent = } else { - mainComponent = + mainComponent = } return ( diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 911ccb6..9ccbc9f 100644 --- a/client/src/components/Level.tsx +++ b/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 Editor from 'lean4web/client/src/Editor' +import { LeanClient } from 'lean4web/client/src/editor/leanclient'; +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(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) { - rpcConnection.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, rpcConnection]) + const uri = monaco.Uri.parse('file:///LeanProject/Level1.lean') + const model = monaco.editor.createModel('', 'lean4', uri) + const editor = monaco.editor.create(codeviewRef.current!, { + model, + glyphMargin: true, + lightbulb: { + enabled: true + }, + unicodeHighlight: { + 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 - {}} - value={""} onDidChangeContent={() => {}}/> +
{/* */} diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx index 2efa1aa..b28eb98 100644 --- a/client/src/components/Welcome.tsx +++ b/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("initialize") -const initializedNotificationType = new rpc.NotificationType0("initialized") -const infoRequestType = new rpc.RequestType1("info") - -function Welcome({ rpcConnection, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) { +function Welcome({ leanClient, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) { const [leanData, setLeanData] = useState(null) useEffect(() => { - if (rpcConnection) { // Will run in the beginning as soon as RPC connection is established - rpcConnection.sendRequest(initializeRequestType).then((res: any) => { - rpcConnection.onRequest("client/registerCapability", () => {}) - rpcConnection.sendNotification(initializedNotificationType) - rpcConnection.sendRequest(infoRequestType, "hello").then((res: infoResultType) =>{ - setLeanData(res) - setNbLevels(res.nb_levels) - setTitle(res.title) - document.title = res.title - setConclusion(res.conclusion) - }); + if (!leanClient) return; + + const getInfo = async () => { + await leanClient.start() // TODO: need a way to wait for start without restarting + leanClient.sendRequest("info", "hello").then((res: infoResultType) =>{ + setLeanData(res) + setNbLevels(res.nb_levels) + setTitle(res.title) + document.title = res.title + setConclusion(res.conclusion) }); } - }, [rpcConnection, setLeanData, setNbLevels, setTitle, setConclusion]) + getInfo() + }, [leanClient]) let content if (leanData) { diff --git a/package-lock.json b/package-lock.json index 2764345..51723c2 100644 --- a/package-lock.json +++ b/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", diff --git a/package.json b/package.json index 4a4980e..a63fe73 100644 --- a/package.json +++ b/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",