display all proof steps in command line modus

client/src/components/infoview/command_line.tsx

@@ -13,8 +13,13 @@ 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 { InteractiveDiagnostic, getInteractiveDiagnostics } from '@leanprover/infoview-api';
+import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
+import { useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 
-import { InputModeContext, MonacoEditorContext } from './context'
+import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context'
+import { goalsToString } from './goals'
+import { InteractiveGoals } from './rpc_api'
 
 /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
 
@@ -58,10 +63,14 @@ config.autoClosingPairs = config.autoClosingPairs.map(
 )
 monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
+/** The input field */
 export function CommandLine() {
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
+  const model = editor.getModel()
+  const uri = model.uri.toString()
+
   const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
 
@@ -69,26 +78,108 @@ export function CommandLine() {
 
   const inputRef = useRef()
 
+  // The context storing all information about the current proof
+  const {proof, setProof} = React.useContext(ProofContext)
+
+  // TODO: does the position matter at all?
+  const rpcSess = useRpcSessionAtPos({uri: uri, line: 1, character: 1})
+
+  /** Load all goals an messages of the current proof (line-by-line) and save
+   * the retrieved information into context (`ProofContext`)
+   */
+  const loadAllGoals = React.useCallback(() => {
+    let goalCalls = []
+    let msgCalls = []
+
+    // For each line of code ask the server for the goals and the messages on this line
+    for (let i = 0; i < model.getLineCount(); i++) {
+      goalCalls.push(
+        rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
+      )
+      msgCalls.push(
+        getInteractiveDiagnostics(rpcSess, {start: i, end: i+1})
+      )
+    }
+
+    // Wait for all these requests to be processed before saving the results
+    Promise.all(goalCalls).then((steps : InteractiveGoals[]) => {
+      Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
+        let tmpProof : ProofStep[] = []
+
+        steps.map((goals, i) => {
+          // The first step has an empty command and therefore also no error messages
+          let messages = i ? diagnostics[i-1] : []
+
+          // Filter out the 'unsolved goals' message
+          messages = messages.filter((msg) => {
+            return !("append" in msg.message &&
+              "text" in msg.message.append[0] &&
+              msg.message.append[0].text === "unsolved goals")
+          })
+
+          // TODO: Check what happens if the code gets into a bad state and no goals are available
+          if (!goals) {
+            tmpProof.push({
+              command: i ? model.getLineContent(i) : '',
+              goals: [],
+              hints: [],
+              errors: messages
+            } as ProofStep)
+          } else {
+
+            console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
+            console.debug(`Goals: (${i}): `, goalsToString(goals)) //
+            console.debug(`Hints: (${i}): `, goals.goals[0]?.hints)
+            console.debug(`Errors: (${i}): `, messages)
+
+            // with no goals there will be no hints
+            let hints = goals.goals.length ? goals.goals[0].hints : []
+
+            tmpProof.push({
+              // the command of the line above. Note that `getLineContent` starts counting
+              // at `1` instead of `zero`. The first ProofStep will have an empty command.
+              command: i ? model.getLineContent(i) : '',
+              // TODO: store correct data
+              goals: goals.goals || [],
+              // only need the hints of the active goals in chat
+              hints: hints,
+              // errors and messages from the server
+              errors: messages
+            } as ProofStep)
+          }
+        })
+        // Save the proof to the context
+        setProof(tmpProof)
+      })
+    })
+  }, [commandLineInput, editor])
+
   // Run the command
   const runCommand = React.useCallback(() => {
-    if (processing) return;
+    if (processing) {return}
     const pos = editor.getPosition()
-    editor.executeEdits("command-line", [{
+    if (commandLineInput) {
-      range: monaco.Selection.fromPositions(
+      setProcessing(true)
-        pos,
+      editor.executeEdits("command-line", [{
-        editor.getModel().getFullModelRange().getEndPosition()
+        range: monaco.Selection.fromPositions(
-      ),
+          pos,
-      text: commandLineInput + "\n",
+          editor.getModel().getFullModelRange().getEndPosition()
-      forceMoveMarkers: false
+        ),
-    }]);
+        text: commandLineInput + "\n",
+        forceMoveMarkers: false
+      }])
+    }
+
     editor.setPosition(pos)
-    setProcessing(true)
   }, [commandLineInput, editor])
 
   useEffect(() => {
     if (oneLineEditor && oneLineEditor.getValue() !== commandLineInput) {
       oneLineEditor.setValue(commandLineInput)
     }
+
+    // TODO: Is this the right place to load the goals once initially?
+    loadAllGoals()
   }, [commandLineInput])
 
   // React when answer from the server comes back
@@ -118,6 +209,7 @@ export function CommandLine() {
         enabled: false
       },
       lineNumbers: 'off',
+      tabSize: 2,
       glyphMargin: false,
       folding: false,
       lineDecorationsWidth: 0,
@@ -146,7 +238,7 @@ export function CommandLine() {
     // Ensure that our one-line editor can only have a single line
     const l = oneLineEditor.getModel().onDidChangeContent((e) => {
       const value = oneLineEditor.getValue()
-      setCommandLineInput(value)
+      setCommandLineInput(value.trim())
       const newValue = value.replace(/[\n\r]/g, '')
       if (value != newValue) {
         oneLineEditor.setValue(newValue)
@@ -161,14 +253,17 @@ export function CommandLine() {
     const l = oneLineEditor.onKeyUp((ev) => {
       if (ev.code === "Enter") {
         runCommand()
+        loadAllGoals() // TODO: instead of loading all goals every time, we could only load the last one
       }
     })
     return () => { l.dispose() }
   }, [oneLineEditor, runCommand])
 
+  /** Process the entered command */
   const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
     ev.preventDefault()
     runCommand()
+    loadAllGoals() // TODO: instead of loading all goals every time, we could only load the last one
   }
 
   return <div className="command-line">
@@ -176,7 +271,9 @@ export function CommandLine() {
         <div className="command-line-input-wrapper">
           <div ref={inputRef} className="command-line-input" />
         </div>
-        <button type="submit" disabled={processing} className="btn btn-inverted"><FontAwesomeIcon icon={faWandMagicSparkles} /> Execute</button>
+        <button type="submit" disabled={processing} className="btn btn-inverted">
+          <FontAwesomeIcon icon={faWandMagicSparkles} /> Execute
+        </button>
       </form>
     </div>
 }

client/src/components/infoview/context.ts

@@ -4,11 +4,45 @@
 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';
+import { InteractiveGoal, InteractiveGoals } from './rpc_api';
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
   null as any)
 
+export type InfoStatus = 'updating' | 'error' | 'ready';
+
+/** One step of the proof */
+export type ProofStep = {
+  /** The command in this step */
+  command : string
+  /** List of goals *after* this command */
+  goals: InteractiveGoal[]     // TODO: Add correct type
+  /** Story relevant messages */
+  hints: any        // TODO: Add correct type
+  /** Errors and warnings */
+  errors: any       // TODO: Add correct type
+}
+
+/** The context storing the proof step-by-step for the command line mode */
+export const ProofContext = React.createContext<{
+  /** The proof consists of multiple steps that are processed one after the other.
+   * In particular multi-line terms like `match`-statements will not be supported.
+   *
+   * Note that the first step will always have `null` as command
+   */
+  proof: ProofStep[],
+  setProof: React.Dispatch<React.SetStateAction<Array<ProofStep>>>
+}>({
+  proof: [],
+  setProof: () => {} // TODO: implement me
+})
+
+
+
+
+
+
+
 // TODO: Is this still used?
 export const HintContext = React.createContext<{
   showHiddenHints : boolean,
@@ -18,25 +52,6 @@ export const HintContext = React.createContext<{
   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;

client/src/components/infoview/goals.tsx

@@ -2,8 +2,7 @@
  * @fileOverview
  *
  * Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx
-*/
+ */
-
 import * as React from 'react'
 import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
 import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
@@ -13,7 +12,6 @@ import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/
 import { InputModeContext } from './context';
 import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api';
 
-
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
     return h.indexOf('✝') >= 0;
@@ -140,6 +138,9 @@ interface ProofDisplayProps {
 export const Goal = React.memo((props: GoalProps) => {
     const { goal, filter, showHints, commandLine } = props
 
+    // TODO: Apparently `goal` can be `undefined`
+    if (!goal) {return <></>}
+
     const filteredList = getFilteredHypotheses(goal.hyps, filter);
     const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
     const locs = React.useContext(LocationsContext)
@@ -182,6 +183,8 @@ export const Goal = React.memo((props: GoalProps) => {
 export const MainAssumptions = React.memo((props: GoalProps2) => {
   const { goals, filter } = props
 
+
+
   const goal = goals[0]
   const filteredList = getFilteredHypotheses(goal.hyps, filter);
   const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;

client/src/components/infoview/main.tsx

@@ -21,11 +21,77 @@ import { levelCompleted, selectCompleted } from '../../state/progress';
 import Markdown from '../markdown';
 
 import { Infos } from './infos';
-import { AllMessages, WithLspDiagnosticsContext } from './messages';
+import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
 import { Goal } from './goals';
-import { InputModeContext, ProofStateContext } from './context';
+import { InputModeContext, ProofContext, ProofStateContext, ProofStep } from './context';
 import { CommandLine } from './command_line';
+import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 
+/** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
+ * always present, or the monaco editor cannot start.
+ */
+export function DualEditor({level, codeviewRef, levelId, worldId, commandLineMode}) {
+  const ec = React.useContext(EditorContext)
+//   const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext)
+
+//   return <div className={hidden ? 'hidden' : ''}>
+//     <ExerciseStatement data={data} />
+//     <div className={`statement ${commandLineMode ? 'hidden' : ''}`}><code>{data?.descrFormat}</code></div>
+//     <div ref={codeviewRef} className={'codeview'}></div>
+//     {ec && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
+
+//   </div>
+// }
+
+  return <>
+    <div className={commandLineMode ? ' hidden' : ''}>
+      <ExerciseStatement data={level?.data} />
+      <div ref={codeviewRef} className={'codeview'}></div>
+    </div>
+    {ec && <DualEditorMain worldId={worldId} levelId={levelId} level={level} commandLineMode={commandLineMode}/>}
+  </>
+}
+
+/* The part of the two editors that can needs the editor connection first */
+function DualEditorMain({worldId, levelId, level, commandLineMode}) {
+  const ec = React.useContext(EditorContext)
+  const gameId = React.useContext(GameIdContext)
+
+  /* Set up updates to the global infoview state on editor events. */
+  const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
+
+  const [allProgress, _1] = useServerNotificationState(
+    '$/lean/fileProgress',
+    new Map<DocumentUri, LeanFileProgressProcessingInfo[]>(),
+    async (params: LeanFileProgressParams) => (allProgress) => {
+        const newProgress = new Map(allProgress);
+        return newProgress.set(params.textDocument.uri, params.processing);
+    }, [])
+  const serverVersion = useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? ''))
+
+  return <>
+  <ConfigContext.Provider value={config}>
+    <VersionContext.Provider value={serverVersion}>
+      <WithRpcSessions>
+        <WithLspDiagnosticsContext>
+          <ProgressContext.Provider value={allProgress}>
+            {/* We need the editor to always there and hidden because
+            the command line edits its content */}
+            { // TODO: Is there any possibility that the editor connection takes a while
+            // and we should show a circular progress here?
+            }
+            {commandLineMode ?
+              <CommandLineInterface world={worldId} level={levelId} data={level?.data}/>
+              :
+              <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />
+            }
+          </ProgressContext.Provider>
+        </WithLspDiagnosticsContext>
+      </WithRpcSessions>
+    </VersionContext.Provider>
+  </ConfigContext.Provider>
+</>
+}
 
 // The mathematical formulation of the statement, supporting e.g. Latex
 // It takes three forms, depending on the precence of name and description:
@@ -106,43 +172,101 @@ export function Main(props: {world: string, level: number}) {
         </div>
     }
 
-    return (
+    return ret
-    <ConfigContext.Provider value={config}>
-        <VersionContext.Provider value={serverVersion}>
-            <WithRpcSessions>
-                <WithLspDiagnosticsContext>
-                    <ProgressContext.Provider value={allProgress}>
-                        {ret}
-                    </ProgressContext.Provider>
-                </WithLspDiagnosticsContext>
-            </WithRpcSessions>
-        </VersionContext.Provider>
-    </ConfigContext.Provider>
-    );
 }
 
-// `codeviewRef`: the codeViewRef. Used to edit the editor's content even if not visible
+const goalFilter = {
-export function EditorInterface({data, codeviewRef, hidden, worldId, levelId, editorConnection}) {
+  reverse: false,
-
+  showType: true,
-  const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext)
+  showInstance: true,
-
+  showHiddenAssumption: true,
-  return <div className={hidden ? 'hidden' : ''}>
+  showLetValue: true
-    <ExerciseStatement data={data} />
+}
-    <div className={`statement ${commandLineMode ? 'hidden' : ''}`}><code>{data?.descrFormat}</code></div>
-    <div ref={codeviewRef} className={'codeview'}></div>
-    {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
 
+/** The display of a single entered lean command */
+function Command({command} : {command: string}) {
+  // The first step will always have an empty command
+  if (!command) {return <></>}
+  return <div className="command">
+    {command}
   </div>
 }
 
+// const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
+//   const ec = React.useContext(EditorContext);
+//   const fname = escapeHtml(basename(uri));
+//   const {line, character} = diag.range.start;
+//   const loc: Location = { uri, range: diag.range };
+//   const text = TaggedText_stripTags(diag.message);
+//   const severityClass = diag.severity ? {
+//       [DiagnosticSeverity.Error]: 'error',
+//       [DiagnosticSeverity.Warning]: 'warning',
+//       [DiagnosticSeverity.Information]: 'information',
+//       [DiagnosticSeverity.Hint]: 'hint',
+//   }[diag.severity] : '';
+//   const title = `Line ${line+1}, Character ${character}`;
+
+//   // Hide "unsolved goals" messages
+//   let message;
+//   if ("append" in diag.message && "text" in diag.message.append[0] &&
+//     diag.message?.append[0].text === "unsolved goals") {
+//       message = diag.message.append[0]
+//   } else {
+//       message = diag.message
+//   }
+
+//   const { commandLineMode } = React.useContext(InputModeContext)
+
+//   return (
+//   // <details open>
+//       // <summary className={severityClass + ' mv2 pointer'}>{title}
+//       //     <span className="fr">
+//       //         <a className="link pointer mh2 dim codicon codicon-go-to-file"
+//       //            onClick={e => { e.preventDefault(); void ec.revealLocation(loc); }}
+//       //            title="reveal file location"></a>
+//       //         <a className="link pointer mh2 dim codicon codicon-quote"
+//       //            data-id="copy-to-comment"
+//       //            onClick={e => {e.preventDefault(); void ec.copyToComment(text)}}
+//       //            title="copy message to comment"></a>
+//       //         <a className="link pointer mh2 dim codicon codicon-clippy"
+//       //            onClick={e => {e.preventDefault(); void ec.api.copyToClipboard(text)}}
+//       //            title="copy message to clipboard"></a>
+//       //     </span>
+//       // </summary>
+//       <div className={severityClass + ' ml1 message'}>
+//           {!commandLineMode && <p className="mv2">{title}</p>}
+//           <pre className="font-code pre-wrap">
+//               <InteractiveMessage fmt={message} />
+//           </pre>
+//       </div>
+//   // </details>
+//   )
+// }, fastIsEqual)
+
+/** The tabs of goals that lean ahs after the command of this step has been processed */
+function GoalsTab({proofStep} : {proofStep: ProofStep}) {
+  const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
+
+  return <div>
+    <div className="tab-bar">
+      {proofStep.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">
+      <Goal commandLine={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
+    </div>
+  </div>
+}
+
+/** The interface in command line mode */
 export function CommandLineInterface(props: {world: string, level: number, data: LevelInfo}) {
 
-  const ec = React.useContext(EditorContext);
+  const ec = React.useContext(EditorContext)
   const gameId = React.useContext(GameIdContext)
-
+  const {proof} = React.useContext(ProofContext)
-  const proofStateContext = React.useContext(ProofStateContext)
-
-  const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
 
   const dispatch = useAppDispatch()
 
@@ -187,8 +311,6 @@ 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);
@@ -206,39 +328,28 @@ export function CommandLineInterface(props: {world: string, level: number, data:
           {/* {completed && <div className="level-completed">Level completed! 🎉</div>} */}
           <div className="content">
             <ExerciseStatement data={props.data} />
-            <Infos />
+            {/* <Infos /> */}
             <div className="tmp-pusher"></div>
-            <div className="tab-bar">
+            {proof.map((step, i) => {
-              {proofStateContext.proofState.goals?.goals.map((goal, i) =>
+              if (i == proof.length - 1 && step.errors.length) {
-                <div className={`tab ${i == (selectedGoal) ? "active": ""}`}
+                // if the last command contains an error, we should not display it
-                    onClick={() => { setSelectedGoal(i) }}>
+                // as it will be overwritten by the next entered command
-                  {i ? `Goal ${i+1}` : "Active Goal"}
+                return <div>
-                </div>)}
+                <Errors errors={step.errors} commandLineMode={true}/>
-            </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>
+              else {
+                return <div className="step">
+                  <Command command={step.command} />
+                  <Errors errors={step.errors} commandLineMode={true}/>
+                  <GoalsTab proofStep={step} />
+                </div>
+              }
+            })}
           </div>
           <CommandLine />
       </div>
   }
 
-  return <>
+  return ret
-    {/* <button className="btn" onClick={handleUndo} disabled={!canUndo}><FontAwesomeIcon icon={faRotateLeft} /> Undo</button> */}
-    <ConfigContext.Provider value={config}>
-      <VersionContext.Provider value={serverVersion}>
-        <WithRpcSessions>
-          <WithLspDiagnosticsContext>
-            <ProgressContext.Provider value={allProgress}>
-              {ret}
-            </ProgressContext.Provider>
-          </WithLspDiagnosticsContext>
-        </WithRpcSessions>
-      </VersionContext.Provider>
-    </ConfigContext.Provider>
-  </>
-
-
 }

client/src/components/infoview/messages.tsx

@@ -17,6 +17,44 @@ interface MessageViewProps {
     diag: InteractiveDiagnostic;
 }
 
+/** A list of messages (info/warning/error) that are produced after this command */
+function Error({error, commandLineMode} : {error : InteractiveDiagnostic, commandLineMode : boolean}) {
+  // The first step will always have an empty command
+
+  const severityClass = error.severity ? {
+    [DiagnosticSeverity.Error]: 'error',
+    [DiagnosticSeverity.Warning]: 'warning',
+    [DiagnosticSeverity.Information]: 'information',
+    [DiagnosticSeverity.Hint]: 'hint',
+  }[error.severity] : '';
+
+  const {line, character} = error.range.start;
+  const title = `Line ${line+1}, Character ${character}`;
+
+  // Hide "unsolved goals" messages
+  let message;
+  if ("append" in error.message && "text" in error.message.append[0] &&
+  error.message?.append[0].text === "unsolved goals") {
+      message = error.message.append[0]
+  } else {
+      message = error.message
+  }
+
+  return <div className={severityClass + ' ml1 message'}>
+    {!commandLineMode && <p className="mv2">{title}</p>}
+    <pre className="font-code pre-wrap">
+      <InteractiveMessage fmt={message} />
+    </pre>
+  </div>
+}
+
+/** A list of messages (info/warning/error) that are produced after this command */
+export function Errors ({errors, commandLineMode} : {errors : InteractiveDiagnostic[], commandLineMode : boolean}) {
+  return <div>
+    {errors.map((err) => (<Error error={err} commandLineMode={commandLineMode}/>))}
+  </div>
+}
+
 const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
     const ec = React.useContext(EditorContext);
     const fname = escapeHtml(basename(uri));

client/src/components/level.css

@@ -211,3 +211,15 @@ td code  {
   overflow-y: scroll;
   padding: 1em;
 }
+
+/* TODO: Create a nice style and move this to a better place */
+
+.exercise .command {
+  background-color: rgb(167, 167, 167);
+}
+
+.exercise .step {
+  background-color: #ffeb91;
+  margin-top: 5px;
+  margin-bottom: 5px;
+}

client/src/components/level.tsx

@@ -6,7 +6,7 @@ import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
-import { InfoviewApi } from '@leanprover/infoview'
+import { InfoviewApi, defaultInfoviewConfig } from '@leanprover/infoview'
 import { Link, useParams } from 'react-router-dom';
 import { Box, CircularProgress, FormControlLabel, FormGroup, Switch, IconButton } from '@mui/material';
 import MuiDrawer from '@mui/material/Drawer';
@@ -28,7 +28,6 @@ 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 { DocumentPosition } from '../../../node_modules/lean4-infoview/src/infoview/util';
 
 import { GameIdContext } from '../app';
 import { ConnectionContext, useLeanClient } from '../connection';
@@ -38,7 +37,7 @@ 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 { EditorInterface, CommandLineInterface } from './infoview/main'
+import { DualEditor } from './infoview/main'
 import { Hints } from './hints';
 import { HintContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStateContext, ProofStateProps, ProofStep } from './infoview/context';
 
@@ -62,6 +61,10 @@ function PlayableLevel({worldId, levelId}) {
   const chatPanelRef = useRef<HTMLDivElement>(null)
 
   const gameId = React.useContext(GameIdContext)
+
+  // The state variables for the `ProofContext`
+  const [proof, setProof] = useState<Array<ProofStep>>([])
+
   const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
   const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
 
@@ -71,7 +74,6 @@ function PlayableLevel({worldId, levelId}) {
 
   const [showHiddenHints, setShowHiddenHints] = useState(false)
 
-  const [proof, setProof] = useState<Array<ProofStep>>([])
 
   const [proofState, setProofState] = React.useState<ProofStateProps>({
     status: 'updating',
@@ -79,7 +81,7 @@ function PlayableLevel({worldId, levelId}) {
     goals: undefined,
     termGoal: undefined,
     error: undefined,
-})
+  })
 
   const theme = useTheme();
 
@@ -182,6 +184,9 @@ function PlayableLevel({worldId, levelId}) {
 
   const levelTitle = <>{levelId && `Level ${levelId}`}{level?.data?.title && `: ${level?.data?.title}`}</>
 
+  // TODO: with the new design, there is no difference between the introduction and
+  // a hint at the beginning of the proof...
+
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <ProofStateContext.Provider value={{proofState, setProofState}}>
@@ -197,9 +202,9 @@ function PlayableLevel({worldId, levelId}) {
                 <Markdown>{level?.data?.introduction}</Markdown>
               </div>
             }
-            {proofState.goals?.goals.length &&
+            {proof.map((step, i) => {
-              <Hints hints={proofState.goals?.goals[0].hints} showHidden={showHiddenHints}/>
+              return <Hints hints={step.hints} showHidden={showHiddenHints}/>
-            }
+            })}
             {completed &&
               <>
                 <div className="message info">
@@ -216,10 +221,6 @@ function PlayableLevel({worldId, levelId}) {
                   Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>}
               </>
             }
-
-            {/* { hints.map(hint => <div className="message info"><Markdown>{hint.text}</Markdown></div>) } */}
-            {/* TODO: Remove this debugging message: */}
-            {showHiddenHints && <p>Hidden Hints are displayed</p>}
           </div>
           <div className="toggle-hidden-hints">
             <FormControlLabel
@@ -230,19 +231,11 @@ function PlayableLevel({worldId, levelId}) {
         </div>
         <div className="exercise-panel">
           <EditorContext.Provider value={editorConnection}>
-          <MonacoEditorContext.Provider value={editor}>
+            <MonacoEditorContext.Provider value={editor}>
-          <div className="exercise">
+              <div className="exercise">
-            {/* We need the editor to always there and hidden because
+                <DualEditor level={level} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} commandLineMode={commandLineMode} />
-              the command line edits its content */}
+              </div>
-            <EditorInterface data={level?.data} codeviewRef={codeviewRef} hidden={commandLineMode}
+            </MonacoEditorContext.Provider>
-                    worldId={worldId} levelId={levelId} editorConnection={editorConnection}/>
-            { // TODO: Is there any possibility that the editor connection takes a while
-              // and we should show a circular progress here?
-              commandLineMode && editorConnection &&
-                <CommandLineInterface world={worldId} level={levelId} data={level?.data}/>
-            }
-          </div>
-          </MonacoEditorContext.Provider>
           </EditorContext.Provider>
         </div>
         <div className="inventory-panel">