refactor

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,77 @@
+/**
+ *  @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 GameIdContext = React.createContext<string>(undefined);
+
+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/hints.tsx

@@ -1,19 +0,0 @@
-import { GameHint } from "./rpcApi";
-import * as React from 'react';
-import { Alert, FormControlLabel, Switch } from '@mui/material';
-import Markdown from '../Markdown';
-
-export function Hint({hint} : {hint: GameHint}) {
-  return <div className="message info"><Markdown>{hint.text}</Markdown></div>
-}
-
-export function Hints({hints, showHidden} : {hints: GameHint[], showHidden: boolean}) {
-
-  const openHints = hints.filter(hint => !hint.hidden)
-  const hiddenHints = hints.filter(hint => hint.hidden)
-
-  return <>
-    {openHints.map(hint => <Hint hint={hint} />)}
-    {showHidden && hiddenHints.map(hint => <Hint hint={hint} />)}
-  </>
-}

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 { 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 { GameIdContext } from './context';
+import { useAppDispatch, useAppSelector } from '../../state/hooks';
 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 {