diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 48fe7d5..ac5c430 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -29,7 +29,7 @@ import { useStore } from 'react-redux'; import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../node_modules/lean4-infoview/src/infoview/contexts'; import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection'; import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'; -import { Main } from './infoview/main' +import { Main, EditorInterface } from './infoview/main' import type { Location } from 'vscode-languageserver-protocol'; import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' @@ -43,19 +43,22 @@ import { Alert } from '@mui/material'; import { GameIdContext } from '../App'; import { GameHint } from './infoview/rpcApi'; +import { Hints } from './infoview/hints'; export const MonacoEditorContext = React.createContext(null as any); -// TODO: Not used yet export const HintContext = React.createContext<{ + showHiddenHints : boolean, + setShowHiddenHints: React.Dispatch> hints: Array, setHints: React.Dispatch>> }>({ + showHiddenHints: true, + setShowHiddenHints: () => {}, hints: [], setHints: () => {}, }); - export const InputModeContext = React.createContext<{ commandLineMode: boolean, setCommandLineMode: React.Dispatch>, @@ -94,20 +97,6 @@ function ExerciseStatement({data}) { } - -// ref: the codeViewRef. Used to edit the editor's content even if not visible -function EditorInterface({data, codeviewRef, hidden, worldId, levelId, editorConnection}) { - - const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext) - - return
-
{data?.descrFormat}
-
- {editorConnection &&
} - -
-} - function ReducedInterface({worldId, levelId, editorConnection}) { return
{/* */} @@ -130,6 +119,7 @@ function PlayableLevel({worldId, levelId}) { // The array of all shown hints. This excludes introduction and conclusion // TODO: Not used yet const [hints, setHints] = useState(Array) + const [showHiddenHints, setShowHiddenHints] = useState(false) const theme = useTheme(); @@ -239,11 +229,19 @@ function PlayableLevel({worldId, levelId}) {
+ {level?.data?.introduction &&
{level?.data?.introduction}
} + {/* {openHints.map(hint => )} + {hiddenHints.length > 0 && + setShowHints((prev) => !prev)} />} + label="I need help!" + />} + {showHints && hiddenHints.map(hint => )} */} {hints.map(hint =>
{hint.text}
) } @@ -257,16 +255,17 @@ function PlayableLevel({worldId, levelId}) { {level?.data?.conclusion}
} - { hints.map(hint =>
{hint.text}
) } + {/* { hints.map(hint =>
{hint.text}
) } */} + {levelId >= gameInfo.data?.worldSize[worldId] ? : } } +
- @@ -284,7 +283,6 @@ function PlayableLevel({worldId, levelId}) { {/* {editorConnection &&
} */} -
{!level.isLoading && diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index 17918e9..9851c30 100644 --- a/client/src/components/infoview/goals.tsx +++ b/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 = + // const hints = 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) => )}
} {commandLine && commandLineMode && } {!filter.reverse && goalLi} - {showHints && hints} + {/* {showHints && hints} */} }) diff --git a/client/src/components/infoview/hints.tsx b/client/src/components/infoview/hints.tsx index c9df021..e97080c 100644 --- a/client/src/components/infoview/hints.tsx +++ b/client/src/components/infoview/hints.tsx @@ -7,21 +7,13 @@ export function Hint({hint} : {hint: GameHint}) { return
{hint.text}
} -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 => )} - {hiddenHints.length > 0 && - setShowHints((prev) => !prev)} />} - label="I need help!" - />} - {showHints && hiddenHints.map(hint => )} + {showHidden && hiddenHints.map(hint => )} } diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx index 6c4c97a..ad7e2f8 100644 --- a/client/src/components/infoview/info.tsx +++ b/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) diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 39075bd..e90eff6 100644 --- a/client/src/components/infoview/main.tsx +++ b/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}) { ); } + +// `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
+
{data?.descrFormat}
+
+ {editorConnection &&
} + +
+}