Merge branch 'jon_new_layout' into dev

client/src/app.test.js

@@ -1,5 +1,5 @@
 import { render, screen } from '@testing-library/react';
-import App from './App';
+import App from './app';
 
 test('renders learn react link', () => {
   render(<App />);

client/src/app.tsx

@@ -1,5 +1,4 @@
 import * as React from 'react';
-import { useState, useEffect } from 'react';
 import { Outlet, useParams } from "react-router-dom";
 
 import '@fontsource/roboto/300.css';

client/src/components/game_menu.tsx

@@ -1,13 +1,11 @@
 import * as React from 'react'
-import { Button } from './Button'
-import { GameIdContext } from '../App';
-import { useStore } from 'react-redux';
-import { useAppDispatch, useAppSelector } from '../hooks';
-import { useSelector } from 'react-redux';
-
+import { useStore, useSelector } from 'react-redux';
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faDownload, faUpload, faEraser } from '@fortawesome/free-solid-svg-icons'
 
+import { Button } from './button'
+import { GameIdContext } from '../app';
+import { useAppDispatch, useAppSelector } from '../hooks';
 import { deleteProgress, selectProgress, loadProgress, GameProgressState } from '../state/progress';
 
 const downloadFile = ({ data, fileName, fileType }) => {

client/src/components/hints.tsx

@@ -1,7 +1,6 @@
-import { GameHint } from "./rpcApi";
+import { GameHint } from "./infoview/rpc_api";
 import * as React from 'react';
-import { Alert, FormControlLabel, Switch } from '@mui/material';
-import Markdown from '../Markdown';
+import Markdown from './markdown';
 
 export function Hint({hint} : {hint: GameHint}) {
   return <div className="message info"><Markdown>{hint.text}</Markdown></div>

client/src/components/infoview/command_line.tsx

@@ -1,24 +1,20 @@
 import * as React from 'react'
 import { useRef, useState, useEffect } from 'react'
-import { LspDiagnosticsContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
-import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
-import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol';
-import { InputModeContext, MonacoEditorContext } from '../Level'
-
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
-import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
-import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
-
+import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { Registry } from 'monaco-textmate' // peer dependency
 import { wireTmGrammars } from 'monaco-editor-textmate'
-import * as lightPlusTheme from 'lean4web/client/src/lightPlus.json'
+import { DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol';
+import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
+import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
+import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 import * as leanSyntax from 'lean4web/client/src/syntaxes/lean.json'
 import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.json'
 import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json'
 import languageConfig from 'lean4/language-configuration.json';
 
+import { InputModeContext, MonacoEditorContext } from './context'
 
 /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
 

client/src/components/infoview/context.ts

@@ -0,0 +1,75 @@
+/**
+ *  @fileOverview This file contains the the react contexts used in the project.
+ */
+import * as React from 'react';
+import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
+import { InteractiveDiagnostic, InteractiveTermGoal } from '@leanprover/infoview-api';
+import { InteractiveGoals } from './rpc_api';
+
+export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
+  null as any)
+
+// TODO: Is this still used?
+export const HintContext = React.createContext<{
+  showHiddenHints : boolean,
+  setShowHiddenHints: React.Dispatch<React.SetStateAction<boolean>>
+}>({
+  showHiddenHints: true,
+  setShowHiddenHints: () => {},
+});
+
+export type InfoStatus = 'updating' | 'error' | 'ready';
+
+export type ProofStep = {
+  // TODO: Add correct types
+  command : string
+  goals: string
+  hints: string
+  errors: string
+}
+
+export const ProofContext = React.createContext<{
+  // The first entry will always have an empty/undefined command
+  proof: ProofStep[],
+  setProof: React.Dispatch<React.SetStateAction<Array<ProofStep>>>
+}>({
+  proof: [],
+  setProof: () => {}
+})
+
+export interface ProofStateProps {
+  // pos: DocumentPosition;
+  status: InfoStatus;
+  messages: InteractiveDiagnostic[];
+  goals?: InteractiveGoals;
+  termGoal?: InteractiveTermGoal;
+  error?: string;
+  // userWidgets: UserWidgetInstance[];
+  // rpcSess: RpcSessionAtPos;
+  // triggerUpdate: () => Promise<void>;
+}
+
+export const ProofStateContext = React.createContext<{
+  proofState : ProofStateProps,
+  setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
+}>({
+  proofState : {
+    status: 'updating',
+    messages: [],
+    goals: undefined,
+    termGoal: undefined,
+    error: undefined},
+  setProofState: () => {},
+});
+
+export const InputModeContext = React.createContext<{
+  commandLineMode: boolean,
+  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
+  commandLineInput: string,
+  setCommandLineInput: React.Dispatch<React.SetStateAction<string>>
+}>({
+  commandLineMode: true,
+  setCommandLineMode: () => {},
+  commandLineInput: "",
+  setCommandLineInput: () => {},
+});

client/src/components/infoview/goals.tsx

@@ -6,10 +6,9 @@ import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_strip
 import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
 import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpcApi';
-import { Hints } from './hints';
-import { CommandLine } from './CommandLine';
-import { InputModeContext } from '../Level';
+import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api';
+import { InputModeContext } from './context';
+
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -231,6 +230,7 @@ export const OtherGoals = React.memo((props: GoalProps2) => {
   </>
 })
 
+
 export const ProofDisplay = React.memo((props : ProofDisplayProps) => {
   const { proof } = props
   const steps = proof.match(/.+/g)

client/src/components/infoview/info.tsx

@@ -1,24 +1,25 @@
 /* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/info.tsx */
 
 import * as React from 'react';
+import { CircularProgress } from '@mui/material';
+
+
 import type { Location, Diagnostic } from 'vscode-languageserver-protocol';
 
-import { goalsToString, Goal, MainAssumptions, OtherGoals, FilteredGoals, ProofDisplay } from './goals'
-import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound,
-    mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util';
-import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
-import { AllMessages, lspDiagToInteractive, MessagesList } from './messages';
 import { getInteractiveTermGoal, InteractiveDiagnostic,
     UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
     RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api';
-import { InteractiveGoal, InteractiveGoals } from './rpcApi';
+import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound,
+    mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util';
+import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/infoview/userWidget'
 import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
-import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
-import { CircularProgress } from '@mui/material';
-import { InputModeContext, MonacoEditorContext, HintContext, ProofStateProps, InfoStatus, ProofStateContext } from '../Level'
-import { Hint } from './hints';
+
+import { AllMessages, lspDiagToInteractive, MessagesList } from './messages';
+import { goalsToString, Goal, MainAssumptions, OtherGoals, FilteredGoals, ProofDisplay } from './goals'
+import { InteractiveGoal, InteractiveGoals } from './rpc_api';
+import { InputModeContext, MonacoEditorContext, HintContext, ProofStateProps, InfoStatus, ProofStateContext } from './context'
 
 
 type InfoKind = 'cursor' | 'pin';
@@ -127,7 +128,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
           <div className="goals-section">
             { goals &&  goals.goals.length > 0 && <>
               <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
-              {/* <ProofDisplay proof={proof}/> */}
+              <ProofDisplay proof={proof}/>
               <OtherGoals filter={goalFilter} goals={goals.goals} />
             </>}
           </div>

client/src/components/infoview/infoview.css

@@ -64,7 +64,7 @@
   flex-direction: column;
 }
 
-.command-line .command-line-input{
+.command-line .command-line-input {
   flex: 1;
 }
 
@@ -128,3 +128,14 @@
   border-radius: 1em;
   padding: 0.6em;
 }
+
+
+/* Push the goals to the bottom for now, until we insert the proof history above. */
+.commandline-interface .content {
+  display: flex;
+  flex-direction: column;
+}
+
+.commandline-interface .content .tmp-pusher {
+  flex: 1;
+}

client/src/components/infoview/main.tsx

@@ -4,26 +4,28 @@ import * as React from 'react';
 import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol';
 
 import 'tachyons/css/tachyons.css';
-// import '@vscode/codicons/dist/codicon.ttf';
 import '@vscode/codicons/dist/codicon.css';
 import '../../../../node_modules/lean4-infoview/src/infoview/index.css';
 import './infoview.css'
 
 import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api';
-
-import { Infos } from './infos';
-import { AllMessages, WithLspDiagnosticsContext } from './messages';
 import { useClientNotificationEffect, useServerNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { WithRpcSessions } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infoview/serverVersion';
+
+import { GameIdContext } from '../../app';
 import { useAppDispatch, useAppSelector } from '../../hooks';
-import { levelCompleted, selectCompleted } from '../../state/progress';
-import { GameIdContext } from '../../App';
-import { InputModeContext } from '../Level';
-import { CommandLine } from './CommandLine';
-import Markdown from '../Markdown';
 import { LevelInfo } from '../../state/api';
+import { levelCompleted, selectCompleted } from '../../state/progress';
+import Markdown from '../markdown';
+
+import { Infos } from './infos';
+import { AllMessages, WithLspDiagnosticsContext } from './messages';
+import { Goal } from './goals';
+import { InputModeContext, ProofStateContext } from './context';
+import { CommandLine } from './command_line';
+
 
 // The mathematical formulation of the statement, supporting e.g. Latex
 // It takes three forms, depending on the precence of name and description:
@@ -138,6 +140,10 @@ export function CommandLineInterface(props: {world: string, level: number, data:
   const ec = React.useContext(EditorContext);
   const gameId = React.useContext(GameIdContext)
 
+  const proofStateContext = React.useContext(ProofStateContext)
+
+  const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
+
   const dispatch = useAppDispatch()
 
   // Mark level as completed when server gives notification
@@ -181,6 +187,8 @@ export function CommandLineInterface(props: {world: string, level: number, data:
       []
   );
 
+  const goalFilter = { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }
+
   const serverVersion =
       useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? ''))
   const serverStoppedResult = useEventResult(ec.events.serverStopped);
@@ -199,6 +207,19 @@ export function CommandLineInterface(props: {world: string, level: number, data:
           <div className="content">
             <ExerciseStatement data={props.data} />
             <Infos />
+            <div className="tmp-pusher"></div>
+            <div className="tab-bar">
+              {proofStateContext.proofState.goals?.goals.map((goal, i) =>
+                <div className={`tab ${i == (selectedGoal) ? "active": ""}`}
+                    onClick={() => { setSelectedGoal(i) }}>
+                  {i ? `Goal ${i+1}` : "Active Goal"}
+                </div>)}
+            </div>
+            <div className="goal-tab vscode-light">
+              {proofStateContext.proofState.goals?.goals?.length &&
+                <Goal commandLine={false} filter={goalFilter} goal={proofStateContext.proofState.goals.goals[selectedGoal]} />
+              }
+            </div>
           </div>
           <CommandLine />
       </div>

client/src/components/infoview/messages.tsx

@@ -1,16 +1,16 @@
-import * as React from 'react';
-import fastIsEqual from 'react-fast-compare';
-import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol';
+import * as React from 'react'
+import fastIsEqual from 'react-fast-compare'
+import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol'
 
-import { LeanDiagnostic, RpcErrorCode } from '@leanprover/infoview-api';
+import { LeanDiagnostic, RpcErrorCode, getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api'
 
-import { basename, escapeHtml, usePausableState, useEvent, addUniqueKeys, DocumentPosition, useServerNotificationState, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util';
-import { ConfigContext, EditorContext, LspDiagnosticsContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
-import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/collapsing';
-import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer';
-import { getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api';
-import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
-import { InputModeContext } from '../Level';
+import { basename, escapeHtml, usePausableState, useEvent, addUniqueKeys, DocumentPosition, useServerNotificationState, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util'
+import { ConfigContext, EditorContext, LspDiagnosticsContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'
+import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/collapsing'
+import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer'
+import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'
+
+import { InputModeContext } from './context'
 
 interface MessageViewProps {
     uri: DocumentUri;

client/src/components/infoview/rpc_api.ts

@@ -1,5 +1,8 @@
-/* This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts ` */
-
+/**
+ *  @fileOverview Defines the interface for the communication with the server.
+ *
+ * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts`
+ */
 import { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
 
 export interface GameHint {

client/src/components/inventory.tsx

@@ -3,9 +3,9 @@ import { useState, useEffect } from 'react';
 import './inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-svg-icons'
-import Markdown from './Markdown';
+import { GameIdContext } from '../app';
+import Markdown from './markdown';
 import { useLoadDocQuery, InventoryTile, LevelInfo } from '../state/api';
-import { GameIdContext } from '../App';
 
 export function Inventory({levelInfo, openDoc } :
   {

client/src/components/landing_page.tsx

@@ -1,19 +1,18 @@
 import * as React from 'react';
-import { useNavigate } from "react-router-dom";
-import { Link } from 'react-router-dom';
-import Markdown from './Markdown';
+import { useNavigate, Link } from "react-router-dom";
 
 import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
-import './LandingPage.css'
-import {PrivacyPolicyPopup} from './PrivacyPolicy'
-
+import './landing_page.css'
 import coverRobo from '../assets/covers/formaloversum.png'
 import bgImage from '../assets/bg.jpg'
 
+import Markdown from './markdown';
+import {PrivacyPolicyPopup} from './privacy_policy'
+
 const flag = {
   'Dutch': '🇳🇱',
   'English': '🇬🇧',

client/src/components/level.tsx

@@ -1,5 +1,7 @@
 import * as React from 'react';
 import { useEffect, useState, useRef } from 'react';
+import Split from 'react-split'
+import { Alert } from '@mui/material';
 import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
@@ -26,74 +28,19 @@ import type { Location } from 'vscode-languageserver-protocol';
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faHome, faArrowRight, faArrowLeft, faRotateLeft } from '@fortawesome/free-solid-svg-icons'
 import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles';
-import Split from 'react-split'
-import { Alert } from '@mui/material';
+import { DocumentPosition } from '../../../node_modules/lean4-infoview/src/infoview/util';
 
-import { Button } from './Button'
-import {Inventory, Documentation} from './Inventory';
-import Markdown from './Markdown';
-import { EditorInterface, CommandLineInterface } from './infoview/main'
-import { Hints } from './infoview/hints';
-import { GameHint, InteractiveGoals } from './infoview/rpcApi';
-import { GameIdContext } from '../App';
+import { GameIdContext } from '../app';
 import { ConnectionContext, useLeanClient } from '../connection';
 import { useAppDispatch, useAppSelector } from '../hooks';
+import { Button } from './button'
+import Markdown from './markdown';
+import {Inventory, Documentation} from './inventory';
 import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api';
 import { changedSelection, codeEdited, selectCode, selectSelections, progressSlice, selectCompleted } from '../state/progress';
-import { DocumentPosition } from '../../../node_modules/lean4-infoview/src/infoview/util';
-import { getInteractiveTermGoal, InteractiveDiagnostic,
-  UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
-  RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api';
-
-export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(null as any);
-
-export const HintContext = React.createContext<{
-  showHiddenHints : boolean,
-  setShowHiddenHints: React.Dispatch<React.SetStateAction<boolean>>
-}>({
-  showHiddenHints: true,
-  setShowHiddenHints: () => {},
-});
-
-export type InfoStatus = 'updating' | 'error' | 'ready';
-
-export interface ProofStateProps {
-  // pos: DocumentPosition;
-  status: InfoStatus;
-  messages: InteractiveDiagnostic[];
-  goals?: InteractiveGoals;
-  termGoal?: InteractiveTermGoal;
-  error?: string;
-  // userWidgets: UserWidgetInstance[];
-  // rpcSess: RpcSessionAtPos;
-  // triggerUpdate: () => Promise<void>;
-}
-
-export const ProofStateContext = React.createContext<{
-  proofState : ProofStateProps,
-  setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
-}>({
-  proofState : {
-    status: 'updating',
-    messages: [],
-    goals: undefined,
-    termGoal: undefined,
-    error: undefined},
-  setProofState: () => {},
-});
-
-
-export const InputModeContext = React.createContext<{
-  commandLineMode: boolean,
-  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
-  commandLineInput: string,
-  setCommandLineInput: React.Dispatch<React.SetStateAction<string>>
-}>({
-  commandLineMode: true,
-  setCommandLineMode: () => {},
-  commandLineInput: "",
-  setCommandLineInput: () => {},
-});
+import { EditorInterface, CommandLineInterface } from './infoview/main'
+import { Hints } from './hints';
+import { HintContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStateContext, ProofStateProps, ProofStep } from './infoview/context';
 
 function Level() {
 
@@ -124,6 +71,8 @@ function PlayableLevel({worldId, levelId}) {
 
   const [showHiddenHints, setShowHiddenHints] = useState(false)
 
+  const [proof, setProof] = useState<Array<ProofStep>>([])
+
   const [proofState, setProofState] = React.useState<ProofStateProps>({
     status: 'updating',
     messages: [],
@@ -238,6 +187,7 @@ function PlayableLevel({worldId, levelId}) {
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <ProofStateContext.Provider value={{proofState, setProofState}}>
     <InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
+    <ProofContext.Provider value={{proof, setProof}}>
     <HintContext.Provider value={{showHiddenHints, setShowHiddenHints}}>
       <LevelAppBar isLoading={level.isLoading} levelTitle={levelTitle} worldId={worldId} levelId={levelId} />
       <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
@@ -307,6 +257,7 @@ function PlayableLevel({worldId, levelId}) {
         </div>
       </Split>
     </HintContext.Provider>
+    </ProofContext.Provider>
     </InputModeContext.Provider>
     </ProofStateContext.Provider>
   </>

client/src/components/message.tsx

@@ -5,7 +5,7 @@ import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
 import { Button, Dialog, DialogContent, DialogContentText, DialogActions } from '@mui/material';
-import Markdown from './Markdown';
+import Markdown from './markdown';
 
 function Message({ isOpen, content, close }) {
 

client/src/components/welcome.tsx

@@ -1,29 +1,22 @@
 import * as React from 'react';
 import { useState, useEffect, useRef } from 'react';
-import './welcome.css'
-import cytoscape, { LayoutOptions } from 'cytoscape'
-import klay from 'cytoscape-klay';
+import { Link } from 'react-router-dom';
 import { useNavigate } from 'react-router-dom';
 import { useSelector } from 'react-redux';
 import Split from 'react-split'
-
-import GameMenu from './GameMenu';
-import {PrivacyPolicy} from './PrivacyPolicy';
+import { Box, Typography, CircularProgress } from '@mui/material';
+import cytoscape, { LayoutOptions } from 'cytoscape'
+import klay from 'cytoscape-klay';
+import './welcome.css'
+import { GameIdContext } from '../app';
+import { selectCompleted } from '../state/progress';
+import { useGetGameInfoQuery } from '../state/api';
+import Markdown from './markdown';
+import GameMenu from './game_menu';
+import {PrivacyPolicy} from './privacy_policy';
 
 cytoscape.use( klay );
 
-import { Box, Typography, CircularProgress } from '@mui/material';
-import { useGetGameInfoQuery } from '../state/api';
-import { Link } from 'react-router-dom';
-import Markdown from './Markdown';
-import { selectCompleted } from '../state/progress';
-import { GameIdContext } from '../App';
-import { Button } from './Button';
-
-import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faDownload, faUpload, faEraser } from '@fortawesome/free-solid-svg-icons'
-
-
 const N = 24          // max number of levels per world
 const R = 800         // radius of a world
 const r = 110          // radius of a level

client/src/connection.ts

@@ -1,9 +1,10 @@
+/**
+ *  @fileOverview todo
+ */
 
+import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { LeanClient } from 'lean4web/client/src/editor/leanclient';
-import * as React from 'react';
-import { useState } from 'react';
-
 
 export class Connection {
   private game: string = undefined // We only keep a connection to a single game at a time
@@ -54,7 +55,7 @@ export const ConnectionContext = React.createContext(null);
 
 export const useLeanClient = (gameId) => {
   const leanClient = connection.getLeanClient(gameId)
-  const [leanClientStarted, setLeanClientStarted] = useState(leanClient.isStarted())
+  const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted())
 
   React.useEffect(() => {
     const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })

client/src/index.tsx

@@ -1,6 +1,6 @@
 import * as React from 'react';
 import { createRoot } from 'react-dom/client';
-import App from './App';
+import App from './app';
 import { ConnectionContext, connection } from './connection'
 import { store } from './state/store';
 import { Provider } from 'react-redux';
@@ -9,10 +9,10 @@ import {
   RouterProvider,
   Route,
 } from "react-router-dom";
-import ErrorPage from './ErrorPage';
-import Welcome from './components/Welcome';
-import LandingPage from './components/LandingPage';
-import Level from './components/Level';
+import ErrorPage from './components/error_page';
+import Welcome from './components/welcome';
+import LandingPage from './components/landing_page';
+import Level from './components/level';
 import { monacoSetup } from 'lean4web/client/src/monacoSetup';
 import { redirect } from 'react-router-dom';
 

client/src/state/api.ts

@@ -1,3 +1,6 @@
+/**
+ * @fileOverview Define API of the server-client communication
+*/
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
 import { Connection } from '../connection'
 

client/src/state/local_storage.ts

@@ -1,14 +1,28 @@
+/**
+ * @fileOverview Load/save the state to the local browser store
+ */
+
 const KEY = "game_progress";
+
+/** Load from browser storage */
 export function loadState() {
   try {
     const serializedState = localStorage.getItem(KEY);
     if (!serializedState) return undefined;
-    return JSON.parse(serializedState);
+    let x = JSON.parse(serializedState);
+    // Complatibilty because `state.level` has been renamed to `x.games`.
+    // TODO: Does this work?
+    if (x.level) {
+      x.games = x.level
+      x.level = undefined
+    }
+    return x
   } catch (e) {
     return undefined;
   }
 }
 
+/** Save to browser storage */
 export async function saveState(state: any) {
   try {
     const serializedState = JSON.stringify(state);

client/src/state/progress.ts

@@ -1,15 +1,10 @@
+/**
+ * @fileOverview Defines the user progress which is loaded from the browser store and kept
+ */
 import { createSlice } from '@reduxjs/toolkit'
 import type { PayloadAction } from '@reduxjs/toolkit'
-import { loadState } from "./localStorage";
+import { loadState } from "./local_storage";
 
-export interface GameProgressState {
-  [world: string] : {[level: number]: LevelProgressState}
-
-}
-
-interface ProgressState {
-  level: {[game: string]: GameProgressState}
-}
 interface Selection {
   selectionStartLineNumber: number,
   selectionStartColumn: number,
@@ -22,18 +17,30 @@ interface LevelProgressState {
   completed: boolean
 }
 
-const initialProgressState = loadState() ?? { level: {} } as ProgressState
-const initalLevelProgressState = {code: "", completed: false} as LevelProgressState
+export interface GameProgressState {
+  [world: string] : {[level: number]: LevelProgressState}
+}
 
-function addLevelProgress(state, action: PayloadAction<{game: string, world: string, level: number}>) {
-  if (!state.level[action.payload.game]) {
-    state.level[action.payload.game] = {}
+/** The progress made on all lean4-games */
+interface ProgressState {
+  games: {[game: string]: GameProgressState}
+}
+
+const initialProgressState: ProgressState = loadState() ?? { games: {} }
+
+// TODO: There was some weird unreproducible bug with removing `as LevelProgressState` here...
+const initalLevelProgressState: LevelProgressState = {code: "", completed: false, selections: []}
+
+/** Add an empty skeleton with progress for the current level */
+function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
+  if (!state.games[action.payload.game]) {
+    state.games[action.payload.game] = {}
   }
-  if (!state.level[action.payload.game][action.payload.world]) {
-    state.level[action.payload.game][action.payload.world] = {}
+  if (!state.games[action.payload.game][action.payload.world]) {
+    state.games[action.payload.game][action.payload.world] = {}
   }
-  if (!state.level[action.payload.game][action.payload.world][action.payload.level]) {
-    state.level[action.payload.game][action.payload.world][action.payload.level] = {...initalLevelProgressState}
+  if (!state.games[action.payload.game][action.payload.world][action.payload.level]) {
+    state.games[action.payload.game][action.payload.world][action.payload.level] = {...initalLevelProgressState}
   }
 }
 
@@ -41,60 +48,77 @@ export const progressSlice = createSlice({
   name: 'progress',
   initialState: initialProgressState,
   reducers: {
-    codeEdited(state, action: PayloadAction<{game: string, world: string, level: number, code: string}>) {
+    /** put edited code in the state and set completed to false */
+    codeEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, code: string}>) {
       addLevelProgress(state, action)
-      state.level[action.payload.game][action.payload.world][action.payload.level].code = action.payload.code
-      state.level[action.payload.game][action.payload.world][action.payload.level].completed = false
+      state.games[action.payload.game][action.payload.world][action.payload.level].code = action.payload.code
+      state.games[action.payload.game][action.payload.world][action.payload.level].completed = false
     },
-    changedSelection(state, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) {
+    /** TODO: ? */
+    changedSelection(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) {
       addLevelProgress(state, action)
-      state.level[action.payload.game][action.payload.world][action.payload.level].selections = action.payload.selections
+      state.games[action.payload.game][action.payload.world][action.payload.level].selections = action.payload.selections
     },
-    levelCompleted(state, action: PayloadAction<{game: string, world: string, level: number}>) {
+    /** mark level as completed */
+    levelCompleted(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
       addLevelProgress(state, action)
-      state.level[action.payload.game][action.payload.world][action.payload.level].completed = true
+      state.games[action.payload.game][action.payload.world][action.payload.level].completed = true
     },
-    deleteProgress(state, action: PayloadAction<{game: string}>) {
-      state.level[action.payload.game] = {}
+    /** delete all progress for this game */
+    deleteProgress(state: ProgressState, action: PayloadAction<{game: string}>) {
+      state.games[action.payload.game] = {}
     },
-    loadProgress(state, action: PayloadAction<{game: string, data:GameProgressState}>) {
+    /** delete progress for this level */
+    deleteLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
+      addLevelProgress(state, action)
+      state.games[action.payload.game][action.payload.world][action.payload.level] = initalLevelProgressState
+    },
+    /** load progress, e.g. from external import */
+    loadProgress(state: ProgressState, action: PayloadAction<{game: string, data:GameProgressState}>) {
       console.debug(`setting data to:\n ${action.payload.data}`)
-      state.level[action.payload.game] = action.payload.data
+      state.games[action.payload.game] = action.payload.data
     },
   }
 })
 
+/** if the level does not exist, return default values */
 export function selectLevel(game: string, world: string, level: number) {
   return (state) =>{
-    if (!state.progress.level[game]) { return initalLevelProgressState }
-    if (!state.progress.level[game][world]) { return initalLevelProgressState }
-    if (!state.progress.level[game][world][level]) { return initalLevelProgressState }
-    return state.progress.level[game][world][level]
+    if (!state.progress.games[game]) { return initalLevelProgressState }
+    if (!state.progress.games[game][world]) { return initalLevelProgressState }
+    if (!state.progress.games[game][world][level]) { return initalLevelProgressState }
+    return state.progress.games[game][world][level]
   }
 }
 
+/** return the code of the current level */
 export function selectCode(game: string, world: string, level: number) {
   return (state) => {
     return selectLevel(game, world, level)(state).code
   }
 }
 
+/** return the selections made in the current level */
 export function selectSelections(game: string, world: string, level: number) {
   return (state) => {
     return selectLevel(game, world, level)(state).selections
   }
 }
 
+/** return whether the current level is clompleted */
 export function selectCompleted(game: string, world: string, level: number) {
   return (state) => {
     return selectLevel(game, world, level)(state).completed
   }
 }
 
+/** return progress for the current game if it exists */
 export function selectProgress(game: string) {
   return (state) => {
-    return state.progress.level[game] ?? null
+    return state.progress.games[game] ?? null
   }
 }
 
-export const { changedSelection, codeEdited, levelCompleted, deleteProgress, loadProgress } = progressSlice.actions
+/** Export actions to modify the progress */
+export const { changedSelection, codeEdited, levelCompleted, deleteProgress,
+  deleteLevelProgress, loadProgress } = progressSlice.actions

client/src/state/store.ts

@@ -1,10 +1,14 @@
+/**
+ * @fileOverview configure the store and save the state periodically to the browser storage
+*/
 import { configureStore } from '@reduxjs/toolkit';
+import { debounce } from "debounce";
+
 import { connection } from '../connection'
-import thunkMiddleware from 'redux-thunk'
 import { apiSlice } from './api'
 import { progressSlice } from './progress'
-import { saveState } from "./localStorage";
-import { debounce } from "debounce";
+import { saveState } from "./local_storage";
+
 
 export const store = configureStore({
   reducer: {
@@ -20,10 +24,11 @@ export const store = configureStore({
     }).concat(apiSlice.middleware),
 });
 
-// Save progress in local storage
+/**
+ * Save progress in local storage once each 800ms.
+ * This is for better performance when multiple changes occur in a short time
+ */
 store.subscribe(
-  // we use debounce to save the state once each 800ms
-  // for better performances in case multiple changes occur in a short time
   debounce(() => {
     saveState(store.getState()[progressSlice.name]);
   }, 800)

package-lock.json

@@ -12,6 +12,7 @@
         "@emotion/styled": "^11.10.5",
         "@fontsource/roboto": "^4.5.8",
         "@fontsource/roboto-mono": "^4.5.8",
+        "@leanprover/infoview": "^0.4.3",
         "@mui/icons-material": "^5.11.0",
         "@mui/material": "^5.11.1",
         "@reduxjs/toolkit": "^1.9.1",
@@ -51,6 +52,7 @@
         "@pmmmwh/react-refresh-webpack-plugin": "^0.5.10",
         "@redux-devtools/core": "^3.13.1",
         "@testing-library/react": "^13.4.0",
+        "@types/debounce": "^1.2.1",
         "babel-loader": "^8.3.0",
         "concurrently": "^7.6.0",
         "css-loader": "^6.7.3",
@@ -2095,9 +2097,9 @@
       }
     },
     "node_modules/@leanprover/infoview": {
-      "version": "0.4.2",
-      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.2.tgz",
-      "integrity": "sha512-Bj+q/7n1xlnpRd4xsJ75uikZPwW5id/G4G1JPqhbbfMacTwAgzLNFaqJhzBrIUuF5nxJYGKRqRIeFtkalGxJ0g==",
+      "version": "0.4.3",
+      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.3.tgz",
+      "integrity": "sha512-SufdOr2myHAbZNUmobfQdAhsEC5H9ddi3KS0z1v/8riWSMm+yJk3u4LxVuzCmmSmV2QxFqtFzn5z+HQqj1Vo7g==",
       "dependencies": {
         "@leanprover/infoview-api": "~0.2.1",
         "@vscode/codicons": "^0.0.32",
@@ -3015,6 +3017,12 @@
       "resolved": "https://registry.npmjs.org/@types/cytoscape/-/cytoscape-3.19.9.tgz",
       "integrity": "sha512-oqCx0ZGiBO0UESbjgq052vjDAy2X53lZpMrWqiweMpvVwKw/2IiYDdzPFK6+f4tMfdv9YKEM9raO5bAZc3UYBg=="
     },
+    "node_modules/@types/debounce": {
+      "version": "1.2.1",
+      "resolved": "https://registry.npmjs.org/@types/debounce/-/debounce-1.2.1.tgz",
+      "integrity": "sha512-epMsEE85fi4lfmJUH/89/iV/LI+F5CvNIvmgs5g5jYFPfhO2S/ae8WSsLOKWdwtoaZw9Q2IhJ4tQ5tFCcS/4HA==",
+      "dev": true
+    },
     "node_modules/@types/debug": {
       "version": "4.1.7",
       "resolved": "https://registry.npmjs.org/@types/debug/-/debug-4.1.7.tgz",

package.json

@@ -8,6 +8,7 @@
     "@emotion/styled": "^11.10.5",
     "@fontsource/roboto": "^4.5.8",
     "@fontsource/roboto-mono": "^4.5.8",
+    "@leanprover/infoview": "^0.4.3",
     "@mui/icons-material": "^5.11.0",
     "@mui/material": "^5.11.1",
     "@reduxjs/toolkit": "^1.9.1",
@@ -47,6 +48,7 @@
     "@pmmmwh/react-refresh-webpack-plugin": "^0.5.10",
     "@redux-devtools/core": "^3.13.1",
     "@testing-library/react": "^13.4.0",
+    "@types/debounce": "^1.2.1",
     "babel-loader": "^8.3.0",
     "concurrently": "^7.6.0",
     "css-loader": "^6.7.3",