Refactor: eliminate old infoview implementations

client/package.json

@@ -11,7 +11,7 @@
     "@fortawesome/free-regular-svg-icons": "^7.2.0",
     "@fortawesome/free-solid-svg-icons": "^7.2.0",
     "@fortawesome/react-fontawesome": "^3.2.0",
-    "@leanprover/infoview": "^0.4.3",
+    "@leanprover/infoview-api": "^0.13.0",
     "@mui/material": "^5.11.1",
     "@reduxjs/toolkit": "^1.9.1",
     "@tanstack/query-core": "^5.90.20",
@@ -20,9 +20,10 @@
     "i18next": "^25.8.18",
     "i18next-http-backend": "^3.0.2",
     "jotai": "^2.13.1",
+    "jotai-effect": "^2.2.3",
     "jotai-location": "^0.6.2",
     "jotai-tanstack-query": "^0.11.0",
-    "lean4monaco": "^1.1.9",
+    "lean4monaco": "^1.1.14",
     "monaco-editor-wrapper": "^5.3.1",
     "react": "^18.2.0",
     "react-country-flag": "^3.1.0",
@@ -34,8 +35,7 @@
     "react-split": "^2.0.14",
     "rehype-katex": "^7.0.1",
     "remark-gfm": "^4.0.1",
-    "remark-math": "^6.0.0",
-    "vscode-lean4": "github:leanprover/vscode-lean4#de0062c"
+    "remark-math": "^6.0.0"
   },
   "devDependencies": {
     "@codingame/esbuild-import-meta-url-plugin": "^1.0.3",

client/src/components/infoview/rpc_api.ts → client/src/api/rpc_api.ts

@@ -1,32 +1,6 @@
-/**
- *  @fileOverview Defines the interface for the communication with the server.
- *
- * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts`
- */
-import type { Range } from 'vscode-languageserver-protocol';
-import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
-import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*';
+import { CodeWithInfos, ContextInfo, FVarId, InteractiveDiagnostic, InteractiveGoalCore, MVarId, TermInfo } from '@leanprover/infoview-api'
 
-export interface InteractiveHypothesisBundle {
-  /** The pretty names of the variables in the bundle. Anonymous names are rendered
-   * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
-   * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */
-  names: string[];
-  fvarIds?: FVarId[];
-  type: CodeWithInfos;
-  val?: CodeWithInfos;
-  isInstance?: boolean;
-  isType?: boolean;
-  isInserted?: boolean;
-  isRemoved?: boolean;
-  isAssumption?: boolean;
-}
 
-export interface InteractiveGoalCore {
-  hyps: InteractiveHypothesisBundle[];
-  type: CodeWithInfos;
-  ctx?: ContextInfo;
-}
 
 export interface InteractiveGoal extends InteractiveGoalCore {
   userName?: string;

client/src/app.tsx

@@ -9,6 +9,17 @@ import '@fontsource/roboto/700.css';
 
 import './css/reset.css';
 import './css/app.css';
+import './css/error_page.css';
+import "./css/infoview.css"
+import "./css/landing_page.css"
+import './css/layout.css';
+import './css/level.css';
+import "./css/popup.css"
+import "./css/tab_bar.css"
+import "./css/typewriter.css"
+import "./css/welcome.css"
+import "./css/world_tree.css"
+
 import i18n from './i18n';
 import { Popup } from './components/popup/popup';
 import { leanMonacoAtom, leanMonacoOptionsAtom } from './store/editor-atoms';
@@ -17,7 +28,6 @@ import { preferencesAtom } from './store/preferences-atoms';
 
 function App({ children }: { children?: React.ReactNode }) {
 
-  const infoviewRef = useRef<HTMLDivElement>(null)
   const [leanMonaco, setLeanMonaco] = useAtom(leanMonacoAtom)
   const [leanMonacoOptions] = useAtom(leanMonacoOptionsAtom)
   const [preferences] = useAtom(preferencesAtom)
@@ -30,7 +40,6 @@ function App({ children }: { children?: React.ReactNode }) {
   useEffect(() => {
     const _leanMonaco = new LeanMonaco()
     setLeanMonaco(_leanMonaco)
-    _leanMonaco.setInfoviewElement(infoviewRef.current!)
 
     ;(async () => {
       await _leanMonaco.start(leanMonacoOptions)
@@ -45,12 +54,12 @@ function App({ children }: { children?: React.ReactNode }) {
   }, [leanMonacoOptions, setLeanMonaco])
 
   return (
-    <div className="app">
+    <>
       <React.Suspense>
         {children}
       </React.Suspense>
       <Popup />
-    </div>
+    </>
   )
 }
 

client/src/components/chat/ChatPanel.tsx

@@ -0,0 +1,134 @@
+import * as React from 'react'
+import { useTranslation } from 'react-i18next'
+import { useGameTranslation } from '../../utils/translation'
+import { useEffect, useRef } from 'react'
+import { useAtom } from 'jotai'
+import { mobileAtom } from '../../store/preferences-atoms'
+import { gameIdAtom, levelIdAtom } from '../../store/location-atoms'
+import { levelInfoAtom } from '../../store/query-atoms'
+import { deletedChatAtom, helpAtom, selectedStepAtom } from '../../store/chat-atoms'
+import { proofAtom } from '../../store/editor-atoms'
+import { DeletedHints, filterHints, Hint, Hints, MoreHelpButton } from '../hints'
+import Markdown from 'react-markdown'
+import { faArrowRight, faHome } from '@fortawesome/free-solid-svg-icons'
+import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
+import { Button } from '../button'
+
+/** Appears on the left of playable levels */
+export function ChatPanel({lastLevel, visible = true}: {lastLevel: boolean, visible: boolean}) {
+  let { t } = useTranslation()
+  const { t : gT } = useGameTranslation()
+  const chatRef = useRef<HTMLDivElement>(null)
+  const [mobile] = useAtom(mobileAtom)
+  const [gameId, navigateToGame] = useAtom(gameIdAtom)
+  const [levelId, navigateToLevel] = useAtom(levelIdAtom)
+  const [{ data: levelInfo }] = useAtom(levelInfoAtom)
+  const [help] = useAtom(helpAtom)
+  const [proof] = useAtom(proofAtom)
+  const [deletedChat] = useAtom(deletedChatAtom)
+  const [selectedStep, setSelectedStep] = useAtom(selectedStepAtom)
+
+  let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
+
+  function toggleSelection(line: number) {
+    return (ev: any) => {
+      console.debug('toggled selection')
+      if (selectedStep == line) {
+        setSelectedStep(undefined)
+      } else {
+        setSelectedStep(line)
+      }
+    }
+  }
+
+  useEffect(() => {
+    // TODO: For some reason this is always called twice
+    console.debug('scroll chat')
+    if (!mobile) {
+      chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0)
+    }
+  }, [proof, help])
+
+  // Scroll to element if selection changes
+  useEffect(() => {
+    if (typeof selectedStep !== 'undefined') {
+      Array.from(chatRef.current!.getElementsByClassName(`step-${selectedStep}`)).map((elem) => {
+        elem.scrollIntoView({block: "center"})
+      })
+    }
+  }, [selectedStep])
+
+  // useEffect(() => {
+  //   // // Scroll to top when loading a new level
+  //   // // TODO: Thats the wrong behaviour probably
+  //   // chatRef.current!.scrollTo(0,0)
+  // }, [gameId, worldId, levelId])
+
+  let introText: Array<string> = gT(levelInfo?.introduction ?? "").split(/\n(\s*\n)+/)
+
+  const focusRef = useRef<HTMLButtonElement>()
+  useEffect(() => {
+   if (proof?.completed) {
+     focusRef.current?.focus()
+   }
+  }, [!!proof?.completed])
+
+  return <div className={`chat-panel ${visible ? '' : 'hidden'}`}>
+    <div ref={chatRef} className="chat">
+      {introText?.filter(it => it.trim()).map(((it, i) =>
+        // Show the level's intro text as hints, too
+        <Hint key={`intro-p-${i}`}
+          hint={{text: it, hidden: false, rawText: it, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
+      ))}
+      {proof?.steps.map((step, i) => {
+        let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
+        if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) {
+          return <Hints key={`hints-${i}`}
+          hints={filteredHints} showHidden={help.has(i)} step={i}
+          selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
+        }
+      })}
+
+      {/* {modifiedHints.map((step, i) => {
+        // It the last step has errors, it will have the same hints
+        // as the second-to-last step. Therefore we should not display them.
+        if (!(i == proof?.steps.length - 1 && withErr)) {
+          // TODO: Should not use index as key.
+          return <Hints key={`hints-${i}`}
+            hints={step} showHidden={showHelp?.has(i)} step={i}
+            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
+        }
+      })} */}
+      <DeletedHints hints={deletedChat}/>
+      {proof?.completed &&
+        <>
+          <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
+            {t("Level completed! 🎉")}
+          </div>
+          {levelInfo?.conclusion?.trim() &&
+            <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
+              <Markdown>{gT(levelInfo?.conclusion ?? "")}</Markdown>
+            </div>
+          }
+        </>
+      }
+    </div>
+    <div className="button-row">
+      {proof?.completed && (lastLevel ?
+        <Button ref={focusRef} onClick={() => {if (gameId) navigateToGame(gameId)}} >
+          <FontAwesomeIcon icon={faHome} />&nbsp;{t("Home")}
+        </Button> :
+        <Button ref={focusRef} onClick={() => {if(levelId !== undefined) navigateToLevel(levelId + 1)}}  >
+          {t("Next")}&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+        </Button>)
+        }
+      <MoreHelpButton selected={null} />
+    </div>
+  </div>
+}
+
+//FIXME: implement
+function lastStepHasErrors(x: any) {return false}
+
+//FIXME: implement
+function isLastStepWithErrors(x: any, y: any) {return false}

client/src/components/chat/IntroPanel.tsx

@@ -0,0 +1,52 @@
+import { useTranslation } from "react-i18next"
+import { useGameTranslation } from "../../utils/translation"
+import { useAtom } from "jotai"
+import { gameIdAtom, levelIdAtom, worldIdAtom } from "../../store/location-atoms"
+import { gameInfoAtom } from "../../store/query-atoms"
+import { readWorldIntroAtom } from "../../store/progress-atoms"
+import { mobileAtom } from "../../store/preferences-atoms"
+import { useEffect, useRef } from "react"
+import React from "react"
+import { Hint } from "../hints"
+import { FontAwesomeIcon } from "@fortawesome/react-fontawesome"
+import { faArrowRight, faHome } from "@fortawesome/free-solid-svg-icons"
+import { Button } from "../button"
+
+/** Appears on the left side of the intro of a world */
+export function IntroPanel() {
+  let { t } = useTranslation()
+  const { t : gT } = useGameTranslation()
+  const [gameId, navigateToGame] = useAtom(gameIdAtom)
+  const [worldId] = useAtom(worldIdAtom)
+  const [{ data: gameInfo }] = useAtom(gameInfoAtom)
+  const [, navigateToLevel] = useAtom(levelIdAtom)
+  const [, readWorldIntro] = useAtom(readWorldIntroAtom)
+
+  const [mobile] = useAtom(mobileAtom)
+
+  let text: Array<string> = gT(gameInfo?.worlds?.nodes[worldId ?? ""]?.introduction ?? "").split(/\n(\s*\n)+/)
+
+  const focusRef = useRef<HTMLButtonElement>()
+  useEffect(() => {
+   focusRef.current?.focus()
+  }, [])
+
+  return <div className="chat-panel">
+    <div className="chat">
+      {text?.filter(t => t.trim()).map(((t, i) =>
+        <Hint key={`intro-p-${i}`}
+          hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={undefined} toggleSelection={undefined} />
+      ))}
+    </div>
+    <div className={`button-row${mobile ? ' mobile' : ''}`}>
+      {gameInfo?.worldSize?.[worldId ?? ""] == 0 ?
+        <Button onClick={() => {if (gameId) navigateToGame(gameId)}}>
+          <FontAwesomeIcon icon={faHome} />
+          </Button> :
+        <Button ref={focusRef} onClick={() => {readWorldIntro(); navigateToLevel(1)}}>
+          {t("Start")}&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+        </Button>
+      }
+    </div>
+  </div>
+}

client/src/components/editor/ExerciseStatement.tsx

@@ -0,0 +1,39 @@
+import React from "react"
+import { useTranslation } from "react-i18next"
+import { useGameTranslation } from "../../utils/translation"
+import { useAtom } from "jotai"
+import { gameIdAtom } from "../../store/location-atoms"
+import { levelInfoAtom } from "../../store/query-atoms"
+import { Markdown } from "../markdown"
+
+/** The mathematical formulation of the statement, supporting e.g. Latex
+ * It takes three forms, depending on the precence of name and description:
+ * - Theorem xyz: description
+ * - Theorem xyz
+ * - Exercises: description
+ *
+ * If `showLeanStatement` is true, it will additionally display the lean code.
+ */
+export function ExerciseStatement({ showLeanStatement = false }) {
+  const { t : gT } = useGameTranslation()
+  const { t } = useTranslation()
+  const [gameId] = useAtom(gameIdAtom)
+  const [{ data: levelInfo }] = useAtom(levelInfoAtom)
+
+  if (!(levelInfo?.descrText || levelInfo?.descrFormat)) { return <></> }
+  return <>
+    <div className="exercise-statement">
+      {levelInfo?.descrText ?
+        <Markdown>
+          {(levelInfo?.displayName ? `**${t("Theorem")}** \`${levelInfo?.displayName}\`: ` : '') + t(levelInfo?.descrText, {ns: gameId})}
+        </Markdown> : levelInfo?.displayName &&
+        <Markdown>
+          {(levelInfo?.displayName ? `**${t("Theorem")}** \`${levelInfo?.displayName}\`: ` : '') + gT(levelInfo?.descrText ?? "")}
+        </Markdown>
+      }
+      {levelInfo?.descrFormat && showLeanStatement &&
+        <p><code className="lean-code">{levelInfo?.descrFormat}</code></p>
+      }
+    </div>
+  </>
+}

client/src/components/editor/GameEditor.tsx

@@ -0,0 +1,26 @@
+import { useAtom } from "jotai"
+import { leanMonacoAtom, typewriterModeAtom } from "../../store/editor-atoms"
+import React, { useEffect, useLayoutEffect, useRef } from "react"
+import { ExerciseStatement } from "./ExerciseStatement"
+import { Typewriter } from "./typewriter/Typewriter"
+
+/**
+ * Note: It is important that the `div` with `codeViewRef` is
+ * always present, or the monaco editor cannot start.
+ */
+export function GameEditor({ codeviewRef } : { codeviewRef: React.MutableRefObject<HTMLDivElement> }) {
+  const infoviewRef = useRef<HTMLDivElement>(null)
+  const [leanMonaco] = useAtom(leanMonacoAtom)
+  const [typewriterMode] = useAtom(typewriterModeAtom)
+
+  useLayoutEffect(() => {
+    leanMonaco?.setInfoviewElement(infoviewRef.current!)
+  })
+
+  return <>
+    <ExerciseStatement showLeanStatement={true} />
+    <div ref={codeviewRef} className='codeview' />
+    <div className='infoview' ref={infoviewRef} />
+    {typewriterMode && <Typewriter />}
+  </>
+}