From d78a8fafa43e9bf5d0fd6325a437ec7d1aa55215 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 30 Nov 2022 12:15:54 +0100
Subject: [PATCH] start custom infoview

---
 client/src/components/Infoview.tsx | 50 ++++++++++++++++++++++++++++++
 client/src/components/Level.tsx    | 17 +++++-----
 2 files changed, 60 insertions(+), 7 deletions(-)
 create mode 100644 client/src/components/Infoview.tsx

diff --git a/client/src/components/Infoview.tsx b/client/src/components/Infoview.tsx
new file mode 100644
index 0000000..53ea5b5
--- /dev/null
+++ b/client/src/components/Infoview.tsx
@@ -0,0 +1,50 @@
+import * as React from 'react';
+import { useEffect, useState, useRef } from 'react';
+import { EditorApi } from '@leanprover/infoview-api'
+import { LeanClient } from 'lean4web/client/src/editor/leanclient';
+import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
+import * as ls from 'vscode-languageserver-protocol'
+
+// TODO: move into Lean 4 web
+function toLanguageServerPosition (pos: monaco.Position): ls.Position {
+  return {line : pos.lineNumber - 1, character: pos.column - 1}
+}
+
+function Infoview({ ready, editor, editorApi, uri, leanClient } : {ready: boolean, editor: monaco.editor.IStandaloneCodeEditor, editorApi: EditorApi, uri: any, leanClient: LeanClient}) {
+  const [rpcSession, setRpcSession] = useState<string>()
+  const [goals, setGoals] = useState<any[]>(null)
+  const liftOff = async () => {
+    const rpcSession = await editorApi.createRpcSession(uri)
+    const fetchInteractiveGoals = () => {
+      const pos = toLanguageServerPosition(editor.getPosition())
+      leanClient.sendRequest("$/lean/rpc/call", {"method":"Lean.Widget.getInteractiveGoals",
+        "params":{"textDocument":{uri}, "position": pos},
+        "sessionId":rpcSession,
+        "textDocument":{uri},
+        "position": pos
+      }).then(({ goals }) => {
+        setGoals(goals)
+      }).catch((err) => {
+        console.error(err)
+      })
+    }
+    setRpcSession(rpcSession)
+    editor.onDidChangeCursorPosition((ev) => {
+      fetchInteractiveGoals()
+    })
+    leanClient.didChange(async (ev) => {
+      fetchInteractiveGoals()
+    })
+  }
+
+  useEffect(() => {
+    if (ready) {
+      liftOff()
+    }
+  }, [ready])
+   // Lean.Widget.getInteractiveGoals
+
+  return (<div>Number of Goals: {goals !== null ? goals.length : "None"}</div>)
+}
+
+export default Infoview
diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 44a5d3c..e141280 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -23,6 +23,7 @@ import { renderInfoview } from '@leanprover/infoview'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import './level.css'
 import { ConnectionContext } from '../connection';
+import Infoview from './Infoview';
 
 interface LevelProps {
   nbLevels: any;
@@ -36,8 +37,8 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
   const [index, setIndex] = useState(level) // Level number
   const [tacticDocs, setTacticDocs] = useState([])
   const [lemmaDocs, setLemmaDocs] = useState([])
-  const [editor, setEditor] = useState(null)
-  const [infoProvider, setInfoProvider] = useState(null)
+  const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
+  const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
   const [infoviewApi, setInfoviewApi] = useState(null)
 
   const [leanData, setLeanData] = useState({goals: []})
@@ -49,6 +50,8 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
   const infoviewRef = useRef<HTMLDivElement>(null)
   const messagePanelRef = useRef<HTMLDivElement>(null)
 
+  const [ready, setReady] = useState(false)
+
   const [message, setMessage] = useState("")
   const [messageOpen, setMessageOpen] = useState(false)
 
@@ -103,21 +106,20 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
     return () => { editor.dispose() }
   }, [])
 
+  const uri = `file:///level${level}`
+
   // The next function will be called when the level changes
   useEffect(() => {
     if (editor) {
-      const uri = monaco.Uri.parse(`file:///level${level}`)
-      const model = monaco.editor.createModel('', 'lean4', uri)
+      const model = monaco.editor.createModel('', 'lean4', monaco.Uri.parse(uri))
 
       editor.setModel(model)
       infoviewApi.serverRestarted(leanClient.initializeResult)
       infoProvider.openPreview(editor, infoviewApi)
+      setReady(true)
 
       new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
-      // setInfoProvider(infoProvider)
-      // setInfoviewApi(infoviewApi)
-
       leanClient.sendRequest("loadLevel", {world: "TestWorld", level}).then((res) => {
         setLevelTitle("Level " + res["index"] + ": " + res["title"])
         setIndex(parseInt(res["index"]))
@@ -156,6 +158,7 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
         <Button disabled={index <= 1} onClick={() => { loadLevel(index - 1) }} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button>
         <Button disabled={index >= nbLevels} onClick={() => { loadLevel(index + 1) }} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
         <div ref={infoviewRef} className="infoview vscode-light"></div>
+        <Infoview ready={ready} leanClient={leanClient} editor={editor} editorApi={infoProvider?.getApi()} uri={uri} />
         {/* <TacticState goals={leanData.goals} errors={errors} lastTactic={lastTactic} completed={completed} /> */}
       </Grid>
     </Grid>