From a32baeb8e722670beaf9efdd0e18a587a75079d0 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 20 Jun 2023 11:39:27 +0200
Subject: [PATCH] move hints to chat

---
 client/src/components/Level.tsx             | 65 ++++++++++++++-------
 client/src/components/infoview/info.tsx     | 43 ++++++--------
 client/src/components/infoview/infoview.css |  2 +-
 client/src/components/infoview/main.tsx     |  1 +
 client/src/components/level.css             |  3 +-
 5 files changed, 67 insertions(+), 47 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index f008905..ee37bca 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -34,26 +34,52 @@ import {Inventory, Documentation} from './Inventory';
 import Markdown from './Markdown';
 import { EditorInterface, CommandLineInterface } from './infoview/main'
 import { Hints } from './infoview/hints';
-import { GameHint } from './infoview/rpcApi';
+import { GameHint, InteractiveGoals } from './infoview/rpcApi';
 import { GameIdContext } from '../App';
 import { ConnectionContext, useLeanClient } from '../connection';
 import { useAppDispatch, useAppSelector } from '../hooks';
 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>>
-  hints: Array<GameHint>,
-  setHints: React.Dispatch<React.SetStateAction<Array<GameHint>>>
 }>({
   showHiddenHints: true,
   setShowHiddenHints: () => {},
-  hints: [],
-  setHints: () => {},
+});
+
+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: () => {},
 });
 
 
@@ -96,11 +122,16 @@ function PlayableLevel({worldId, levelId}) {
   const [commandLineInput, setCommandLineInput] = useState("")
   const [canUndo, setCanUndo] = useState(initialCode.trim() !== "")
 
-  // The array of all shown hints. This excludes introduction and conclusion
-  // TODO: Not used yet
-  const [hints, setHints] = useState(Array<GameHint>)
   const [showHiddenHints, setShowHiddenHints] = useState(false)
 
+  const [proofState, setProofState] = React.useState<ProofStateProps>({
+    status: 'updating',
+    messages: [],
+    goals: undefined,
+    termGoal: undefined,
+    error: undefined,
+})
+
   const theme = useTheme();
 
 
@@ -205,8 +236,9 @@ function PlayableLevel({worldId, levelId}) {
 
   return <>
     <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}}>
-    <HintContext.Provider value={{showHiddenHints, setShowHiddenHints, hints, setHints}}>
+    <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' : ''}`}>
         <div ref={chatPanelRef} className="chat-panel">
@@ -216,15 +248,8 @@ function PlayableLevel({worldId, levelId}) {
                 <Markdown>{level?.data?.introduction}</Markdown>
               </div>
             }
-                {/* {openHints.map(hint => <Hint hint={hint} />)}
-      {hiddenHints.length > 0 &&
-          <FormControlLabel
-            control={<Switch checked={showHints} onChange={() => setShowHints((prev) => !prev)} />}
-            label="I need help!"
-          />}
-      {showHints && hiddenHints.map(hint => <Hint hint={hint} />)} */}
-            {hints.map(hint =>
-              <div className="message info"><Markdown>{hint.text}</Markdown></div>)
+            {proofState.goals?.goals.length &&
+              <Hints hints={proofState.goals?.goals[0].hints} showHidden={showHiddenHints}/>
             }
             {completed &&
               <>
@@ -244,7 +269,6 @@ function PlayableLevel({worldId, levelId}) {
             }
 
             {/* { hints.map(hint => <div className="message info"><Markdown>{hint.text}</Markdown></div>) } */}
-            <Hints hints={hints} showHidden={showHiddenHints}/>
             {/* TODO: Remove this debugging message: */}
             {showHiddenHints && <p>Hidden Hints are displayed</p>}
           </div>
@@ -284,6 +308,7 @@ function PlayableLevel({worldId, levelId}) {
       </Split>
     </HintContext.Provider>
     </InputModeContext.Provider>
+    </ProofStateContext.Provider>
   </>
 }
 
diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx
index 0c15c7d..c57621b 100644
--- a/client/src/components/infoview/info.tsx
+++ b/client/src/components/infoview/info.tsx
@@ -17,11 +17,10 @@ import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-i
 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 } from '../Level'
+import { InputModeContext, MonacoEditorContext, HintContext, ProofStateProps, InfoStatus, ProofStateContext } from '../Level'
 import { Hint } from './hints';
 
 
-type InfoStatus = 'updating' | 'error' | 'ready';
 type InfoKind = 'cursor' | 'pin';
 
 interface InfoPinnable {
@@ -169,18 +168,13 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
 
 interface InfoDisplayProps {
     pos: DocumentPosition;
-    status: InfoStatus;
-    messages: InteractiveDiagnostic[];
-    goals?: InteractiveGoals;
-    termGoal?: InteractiveTermGoal;
-    error?: string;
     userWidgets: UserWidgetInstance[];
     rpcSess: RpcSessionAtPos;
     triggerUpdate: () => Promise<void>;
 }
 
 /** Displays goal state and messages. Can be paused. */
-function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
+function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable) {
     // Used to update the paused state *just once* if it is paused,
     // but a display update is triggered
     const [shouldRefresh, setShouldRefresh] = React.useState<boolean>(false);
@@ -218,7 +212,7 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
     <RpcContext.Provider value={rpcSess}>
     {/* <details open> */}
         {/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */}
-        <div>
+        <div className="vscode-light">
             <InfoDisplayContent {...props} proof={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
         </div>
     {/* </details> */}
@@ -257,8 +251,11 @@ function useIsProcessingAt(p: DocumentPosition): boolean {
 
 function InfoAux(props: InfoProps) {
 
-    // TODO
+    // TODO: proofStateContext is not quite implemented correctly yet.
+    // i.e. there is an asynchronous state in this file that seems to partally overlap
+    // search for `const [state, triggerUpdateCore]`
     const hintContext = React.useContext(HintContext)
+    const proofStateContext = React.useContext(ProofStateContext)
 
     const config = React.useContext(ConfigContext)
 
@@ -294,7 +291,7 @@ function InfoAux(props: InfoProps) {
     // Besides what the server replies with, we also include the inputs (deps) in this type so
     // that the displayed state cannot ever get out of sync by showing an old reply together
     // with e.g. a new `pos`.
-    type InfoRequestResult = Omit<InfoDisplayProps, 'triggerUpdate'>
+    type InfoRequestResult = Omit<ProofStateProps & InfoDisplayProps, 'triggerUpdate'>
     const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((resolve, reject) => {
         const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos));
         const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos))
@@ -393,11 +390,6 @@ function InfoAux(props: InfoProps) {
 
     const [displayProps, setDisplayProps] = React.useState<InfoDisplayProps>({
         pos,
-        status: 'updating',
-        messages: [],
-        goals: undefined,
-        termGoal: undefined,
-        error: undefined,
         userWidgets: [],
         rpcSess,
         triggerUpdate
@@ -410,20 +402,21 @@ function InfoAux(props: InfoProps) {
     React.useEffect(() => {
         if (state.state === 'notStarted')
             void triggerUpdate()
-        else if (state.state === 'loading')
-            setDisplayProps(dp => ({ ...dp, status: 'updating' }))
+        else if (state.state === 'loading') {
+          proofStateContext.setProofState(dp => ({ ...dp, status: 'updating' }))
+          setDisplayProps(dp => ({ ...dp, status: 'updating' }))
+        }
         else if (state.state === 'resolved') {
-            setDisplayProps({ ...state.value, triggerUpdate })
-            // if (state.value.goals) {
-            //   hintContext.setHints(state.value.goals[0]?.hints)
-            // }
-            // NOT Working
-
+          // if (state.value.goals?.goals?.length) {
+          //   hintContext.setHints(state.value.goals.goals[0].hints)
+          // }
+          proofStateContext.setProofState({ ...state.value })
+          setDisplayProps({ ...state.value, triggerUpdate })
         } else if (state.state === 'rejected' && state.error !== 'retry') {
             // The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception.
             console.warn('Unreachable code reached with error: ', state.error)
         }
     }, [state])
 
-    return <InfoDisplay kind={props.kind} onPin={props.onPin} {...displayProps} />
+    return <InfoDisplay kind={props.kind} onPin={props.onPin} {...proofStateContext.proofState} {...displayProps} />
 }
diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css
index 8fa999f..1024033 100644
--- a/client/src/components/infoview/infoview.css
+++ b/client/src/components/infoview/infoview.css
@@ -41,7 +41,7 @@
   padding: 0.5em;
   font-family: var(--ff-primary);
   border-radius: 0.2em;
-  margin: 0.2em 0 0;
+  /* margin: 0.2em 0 0; */
 }
 
 .command-line form {
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index fc91391..38e520b 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -31,6 +31,7 @@ import { LevelInfo } from '../../state/api';
 // - Theorem xyz
 // - Exercises: description
 function ExerciseStatement({data}) {
+  if (!data?.descrText) { return <></> }
   return <div className="exercise-statement"><Markdown>
     {(data?.statementName ? `**Theorem** \`${data?.statementName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}` }
   </Markdown></div>
diff --git a/client/src/components/level.css b/client/src/components/level.css
index ad99469..7494e0b 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -29,7 +29,7 @@
   overflow: auto;
 }
 
-.chat-panel, .infoview, .exercise {
+.chat-panel, .infoview {
   padding-top: 1em;
   padding-bottom: 0;
 }
@@ -209,4 +209,5 @@ td code  {
 .commandline-interface .content {
   flex: 1 1 auto;
   overflow-y: scroll;
+  padding: 1em;
 }