merge again

client/src/components/LeftPanel.tsx

@@ -71,12 +71,12 @@ function LemmaDocs({ lemmas }) {
 function LeftPanel({ spells, inventory }) {
   return (
     <Box>
-      {spells.length > 0 &&
+      {spells && spells.length > 0 &&
         <Paper sx={{ px: 2, py: 1 }}>
           <Typography variant="h5" sx={{ mb: 2 }}>Spell book</Typography>
           {spells.map((spell) => <TacticDoc key={spell.name} tactic={spell} />)}
         </Paper>}
-      {inventory.length > 0 && <LemmaDocs lemmas={inventory} />}
+      {inventory && inventory.length > 0 && <LemmaDocs lemmas={inventory} />}
     </Box>)
 }
 

client/src/components/Level.tsx

@@ -7,12 +7,10 @@ import '@fontsource/roboto/700.css';
 import ReactMarkdown from 'react-markdown';
 import { MathJax } from "better-react-mathjax";
 import { Link as RouterLink } from 'react-router-dom';
-
+import { Box, Button, CircularProgress, FormControlLabel, FormGroup, Switch } from '@mui/material';
-
-import { Button, FormControlLabel, FormGroup, Switch } from '@mui/material';
 import Grid from '@mui/material/Unstable_Grid2';
-
 import LeftPanel from './LeftPanel';
+import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
 import { InfoProvider } from 'lean4web/client/src/editor/infoview';
@@ -23,7 +21,7 @@ import './level.css'
 import { ConnectionContext } from '../connection';
 import Infoview from './Infoview';
 import { useParams } from 'react-router-dom';
-import { MonacoServices } from 'monaco-languageclient';
+import { useLoadLevelQuery } from '../game/api';
 
 
 
@@ -33,52 +31,68 @@ function Level() {
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
 
-  const [tacticDocs, setTacticDocs] = useState([])
-  const [lemmaDocs, setLemmaDocs] = useState([])
-  const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
-  const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
-  const [infoviewApi, setInfoviewApi] = useState(null)
   const [expertInfoview, setExpertInfoview] = useState(false)
 
-
-  const [leanData, setLeanData] = useState({goals: [], description: "Loading..."})
-  const [history, setHistory] = useState([])
-  const [lastTactic, setLastTactic] = useState("")
-  const [introduction, setIntroduction] = useState("")
-  const [description, setDescription] = useState("Loading...")
-  const [ppStatement, setPPStatement] = useState("")
-  const [errors, setErrors] = useState([])
   const codeviewRef = useRef<HTMLDivElement>(null)
   const infoviewRef = useRef<HTMLDivElement>(null)
   const messagePanelRef = useRef<HTMLDivElement>(null)
 
-  const [ready, setReady] = useState(false)
+  useEffect(() => {
+    // Scroll to top when loading a new level
+    messagePanelRef.current!.scrollTo(0,0)
+  }, [levelId])
 
-  const [message, setMessage] = useState("")
+  const connection = React.useContext(ConnectionContext)
-  const [messageOpen, setMessageOpen] = useState(false)
 
+  const level = useLoadLevelQuery({world: worldId, level: levelId})
 
-  const [completed, setCompleted] = useState(false)
+  const {editor, infoProvider} = useLevelEditor(worldId, levelId, codeviewRef, infoviewRef)
 
-  const processResponse = (res:any) => {
+  return <>
-    setLeanData(res);
+    <Box style={level.isLoading ? null : {display: "none"}} display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
-    // setErrors(res.errors);
+    <Grid style={level.isLoading ? {display: "none"} : null} className="level" container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
-    // if (res.message !== "" && res.errors?.length === 0) {
+      <Grid xs={4} className="doc-panel">
-    //   setMessage(res.message)
+        <LeftPanel spells={level?.data?.tactics} inventory={level?.data?.tactics} />
-    //   setMessageOpen(true)
+      </Grid>
-    // }
+      <Grid xs={4} className="main-panel">
-    // if (res.goals?.length === 0 && res.errors?.length === 0) {
+        <div ref={messagePanelRef} className="message-panel">
-    //   setCompleted(true)
+          <MathJax><ReactMarkdown>{level?.data?.introduction}</ReactMarkdown></MathJax>
-    // }
+        </div>
-  }
+        <p><b>Aufgabe:</b></p>
+        <div><MathJax><ReactMarkdown>{level?.data?.descrText}</ReactMarkdown></MathJax></div>
+        <div className="statement"><code>{level?.data?.descrFormat}</code></div>
+          {/*NOTE(TODO): currently this looks bad, so I disabled it. Maybe have a drop-down for it of Syntax highlighting... */}
+        <div ref={codeviewRef} className="codeview"></div>
+      </Grid>
+      <Grid xs={4} className="info-panel">
 
-  useEffect(() => {
+        <Button disabled={levelId <= 1} component={RouterLink} to={`/world/${worldId}/level/${levelId - 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button>
-    // Scroll to top when loading a new level
+        <Button disabled={false} component={RouterLink} to={`/world/${worldId}/level/${levelId + 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
-    messagePanelRef.current!.scrollTo(0,0)
+
-  }, [levelId])
+        <div style={{display: expertInfoview ? 'block' : 'none' }} ref={infoviewRef} className="infoview vscode-light"></div>
+        <div style={{display: expertInfoview ? 'none' : 'block' }}>
+          <Infoview leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />
+        </div>
+        <FormGroup>
+          <FormControlLabel onChange={() => { setExpertInfoview(!expertInfoview) }} control={<Switch />} label="Expert mode" />
+        </FormGroup>
+      </Grid>
+    </Grid>
+    </>
+}
+
+export default Level
+
+
+function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewRef) {
 
   const connection = React.useContext(ConnectionContext)
 
+  const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
+  const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
+  const [infoviewApi, setInfoviewApi] = useState(null)
+
+  // Create Editor
   useEffect(() => {
     const editor = monaco.editor.create(codeviewRef.current!, {
       glyphMargin: true,
@@ -105,83 +119,28 @@ function Level() {
     setInfoProvider(infoProvider)
     setInfoviewApi(infoviewApi)
 
-    return () => { editor.dispose() }
+    return () => { editor.setModel(null); infoProvider.dispose(); }
   }, [])
 
-  const uri = `file:///${worldId}/${levelId}`
+  // Create model when level changes
-
-  // The next function will be called when the level changes
   useEffect(() => {
     connection.startLeanClient().then((leanClient) => {
       if (editor) {
 
-        const model = monaco.editor.createModel('', 'lean4', monaco.Uri.parse(uri))
+        const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
+        const model = monaco.editor.getModel(uri) ??
+          monaco.editor.createModel('', 'lean4', uri)
 
         editor.setModel(model)
         infoviewApi.serverRestarted(leanClient.initializeResult)
         infoProvider.openPreview(editor, infoviewApi)
-        setReady(true)
+        new LeanTaskGutter(infoProvider.client, editor)
 
         new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
-
-
-        leanClient.sendRequest("loadLevel", {world: worldId, level: levelId}).then((res) => {
-          // setLevelTitle("Level " + res["index"] + ": " + res["title"])
-          // setIndex(parseInt(res["index"]))
-          setTacticDocs(res["tactics"])
-          setLemmaDocs(res["lemmas"])
-          setIntroduction(res["introduction"])
-          setDescription(res["description"])
-          setPPStatement(res["ppStatement"])
-          processResponse(res)
-        });
-
-        return () => { model.dispose(); setReady(false) }
       }
     })
 
   }, [editor, levelId, connection])
 
-  function loadLevel(index) {
+  return {editor, infoProvider}
-    setCompleted(false)
-    setHistory([])
-    // setCurLevel(index)
-  }
-
-  return (
-    <Grid className="level" container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
-      <Grid xs={4} className="doc-panel">
-        <LeftPanel spells={tacticDocs} inventory={lemmaDocs} />
-      </Grid>
-      <Grid xs={4} className="main-panel">
-        <div ref={messagePanelRef} className="message-panel">
-          <MathJax><ReactMarkdown>{introduction}</ReactMarkdown></MathJax>
-        </div>
-        <p><b>Aufgabe:</b></p>
-        <div><MathJax><ReactMarkdown>{description}</ReactMarkdown></MathJax></div>
-        {/* <div className="statement"><code>{ppStatement}</code></div>
-          NOTE(TODO): currently this looks bad, so I disabled it. Maybe have a drop-down for it of Syntax highlighting... */}
-        <div ref={codeviewRef} className="codeview">
-          {/* <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} /> */}
-        </div>
-      </Grid>
-      <Grid xs={4} className="info-panel">
-
-        <Button disabled={levelId <= 1} component={RouterLink} to={`/world/${worldId}/level/${levelId - 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button>
-        <Button disabled={false} component={RouterLink} to={`/world/${worldId}/level/${levelId + 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
-
-        <div style={{display: expertInfoview ? 'block' : 'none' }} ref={infoviewRef} className="infoview vscode-light"></div>
-        <div style={{display: expertInfoview ? 'none' : 'block' }}>
-          <Infoview leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />
-        </div>
-        <FormGroup>
-          <FormControlLabel onChange={() => { setExpertInfoview(!expertInfoview) }} control={<Switch />} label="Expert mode" />
-        </FormGroup>
-      </Grid>
-    </Grid>
-  )
 }
-
-export default Level

client/src/game/api.ts

@@ -1,7 +1,7 @@
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
 import { Connection } from '../connection'
 
-interface GameState {
+interface GameInfo {
   title: null|string,
   introduction: null|string,
   worlds: null|{nodes: string[], edges: string[][2]},
@@ -9,6 +9,16 @@ interface GameState {
   conclusion: null|string,
 }
 
+interface LevelInfo {
+  title: null|string,
+  introduction: null|string,
+  index: number,
+  tactics: any[],
+  lemmas: any[],
+  descrText: null|string,
+  descrFormat: null|string,
+}
+
 const customBaseQuery = async (
   args : {method: string, params?: any},
   { signal, dispatch, getState, extra },
@@ -27,12 +37,15 @@ export const gameApi = createApi({
   reducerPath: 'gameApi',
   baseQuery: customBaseQuery,
   endpoints: (builder) => ({
-    getGameInfo: builder.query<GameState, void>({
+    getGameInfo: builder.query<GameInfo, void>({
       query: () => {return {method: 'info', params: {}}},
     }),
+    loadLevel: builder.query<LevelInfo, {world: string, level: number}>({
+      query: ({world, level}) => {return {method: "loadLevel", params: {world, level}}},
+    }),
   }),
 })
 
 // Export hooks for usage in functional components, which are
 // auto-generated based on the defined endpoints
-export const { useGetGameInfoQuery } = gameApi
+export const { useGetGameInfoQuery, useLoadLevelQuery } = gameApi

server/leanserver/GameServer/Commands.lean

@@ -82,8 +82,8 @@ elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : comma
   elabCommand thmStatement
   modifyCurLevel fun level => pure {level with
     goal := sig,
-    description := descr.getString,
+    descrText := descr.getString,
-    ppStatement := match statementName with
+    descrFormat := match statementName with
     | none => "example " ++ (toString <| reprint sig.raw) ++ " := by"
     | some name => (Format.join ["lemma ", reprint name.raw, " ", reprint sig.raw, " := by"]).pretty 10  -- "lemma "  ++ (toString <| reprint name.raw) ++ " " ++ (Format.pretty (reprint sig.raw) 40) ++ " := by"
   } -- Format.pretty <| format thmStatement.raw }

server/leanserver/GameServer/EnvExtensions.lean

@@ -202,7 +202,8 @@ structure GameLevel where
   lemmas: Array LemmaDocEntry := default
   messages: Array GoalMessageEntry := default
   goal : TSyntax `Lean.Parser.Command.declSig := default
-  ppStatement : String := default
+  descrText: String := default
+  descrFormat : String := default
   deriving Inhabited, Repr
 
 /-! ## World -/

server/leanserver/GameServer/Game.lean

@@ -41,8 +41,8 @@ structure LevelInfo where
   tactics: Array TacticDocEntry
   lemmas: Array LemmaDocEntry
   introduction : String
-  description : String
+  descrText : String := ""
-  ppStatement : String
+  descrFormat : String := ""
 deriving ToJson
 
 structure LoadLevelParams where
@@ -70,8 +70,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
             title := lvl.title,
             tactics := lvl.tactics,
             lemmas := lvl.lemmas,
-            description := lvl.description,
+            descrText := lvl.descrText,
-            ppStatement := lvl.ppStatement --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
+            descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
             introduction := lvl.introduction }
       c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
       return true