wip on hints

client/src/components/infoview/goals.tsx

@@ -156,7 +156,7 @@ export const Goal = React.memo((props: GoalProps) => {
     // if (props.goal.isInserted) cn += 'b--inserted '
     // if (props.goal.isRemoved) cn += 'b--removed '
 
-    const hints = <Hints hints={goal.hints} key={goal.mvarId} />
+    // const hints = <Hints hints={goal.hints} key={goal.mvarId} />
     const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
     const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
     const {commandLineMode} = React.useContext(InputModeContext)
@@ -172,7 +172,7 @@ export const Goal = React.memo((props: GoalProps) => {
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
         {commandLine && commandLineMode && <CommandLine />}
         {!filter.reverse && goalLi}
-        {showHints && hints}
+        {/* {showHints && hints} */}
     </div>
 })
 

client/src/components/infoview/hints.tsx

@@ -7,21 +7,13 @@ export function Hint({hint} : {hint: GameHint}) {
   return <div className="message info"><Markdown>{hint.text}</Markdown></div>
 }
 
-export function Hints({hints} : {hints: GameHint[]}) {
-
-
-  const [showHints, setShowHints] = React.useState(false);
+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} />)}
-    {hiddenHints.length > 0 &&
-        <FormControlLabel
-          control={<Switch checked={showHints} onChange={() => setShowHints((prev) => !prev)} />}
-          label="I need help!"
-        />}
-    {showHints && hiddenHints.map(hint => <Hint hint={hint} />)}
+    {showHidden && hiddenHints.map(hint => <Hint hint={hint} />)}
   </>
 }

client/src/components/infoview/info.tsx

@@ -18,6 +18,7 @@ import { GoalsLocation, Locations, LocationsContext } from '../../../../node_mod
 import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
 import { CircularProgress } from '@mui/material';
 import { InputModeContext, MonacoEditorContext, HintContext } from '../Level'
+import { Hint } from './hints';
 
 
 type InfoStatus = 'updating' | 'error' | 'ready';
@@ -255,6 +256,10 @@ function useIsProcessingAt(p: DocumentPosition): boolean {
 }
 
 function InfoAux(props: InfoProps) {
+
+    // TODO
+    const hintContext = React.useContext(HintContext)
+
     const config = React.useContext(ConfigContext)
 
     // eslint-disable-next-line @typescript-eslint/no-non-null-assertion
@@ -409,6 +414,11 @@ function InfoAux(props: InfoProps) {
             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
+
         } 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)

client/src/components/infoview/main.tsx

@@ -20,6 +20,7 @@ import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infov
 import { useAppDispatch, useAppSelector } from '../../hooks';
 import { levelCompleted, selectCompleted } from '../../state/progress';
 import { GameIdContext } from '../../App';
+import { InputModeContext } from '../Level';
 
 
 export function Main(props: {world: string, level: number}) {
@@ -101,3 +102,16 @@ export function Main(props: {world: string, level: number}) {
     </ConfigContext.Provider>
     );
 }
+
+// `codeviewRef`: the codeViewRef. Used to edit the editor's content even if not visible
+export function EditorInterface({data, codeviewRef, hidden, worldId, levelId, editorConnection}) {
+
+  const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext)
+
+  return <div className={hidden ? 'hidden' : ''}>
+    <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} />}
+
+  </div>
+}