diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx index 10fe55e..e488464 100644 --- a/client/src/components/hints.tsx +++ b/client/src/components/hints.tsx @@ -68,12 +68,12 @@ function hasHiddenHints(step: InteractiveGoalsWithHints): boolean { } -export function MoreHelpButton() { +export function MoreHelpButton({selected=null} : {selected?: number}) { const {proof, setProof} = React.useContext(ProofContext) const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext) - let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1) + let k = (selected === null) ? (proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected const activateHiddenHints = (ev) => { // If the last step (`k`) has errors, we want the hidden hints from the diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 3e768fa..74c8df1 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -155,7 +155,20 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) { const {worldId, levelId} = React.useContext(WorldLevelIdContext) const { proof, setProof } = React.useContext(ProofContext) + const {selectedStep, setSelectedStep} = React.useContext(SelectionContext) + const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext) + + function toggleSelection(line: number) { + return (ev) => { + console.debug('toggled selection') + if (selectedStep == line) { + setSelectedStep(undefined) + } else { + setSelectedStep(line) + } + } + } console.debug(`template: ${props.data?.template}`) // React.useEffect (() => { @@ -182,6 +195,19 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) { const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri); + const curPos: DocumentPosition | undefined = + useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) + + // Effect when the cursor changes in the editor + React.useEffect(() => { + // TODO: this is a bit of a hack and will yield unexpected behaviour if lines + // are indented. + let newPos = curPos?.line + (curPos?.character == 0 ? 0 : 1) + + // scroll the chat along + setSelectedStep(newPos) + }, [curPos]) + useClientNotificationEffect( 'textDocument/didClose', (params: DidCloseTextDocumentParams) => { @@ -208,6 +234,11 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) { ret =
{proof.completed &&
Level completed! 🎉
} + +
} diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx index 700343e..dd2721b 100644 --- a/client/src/components/infoview/messages.tsx +++ b/client/src/components/infoview/messages.tsx @@ -194,16 +194,24 @@ export function AllMessages() { */} - + {/* */} ) } /** We factor out the body of {@link AllMessages} which lazily fetches its contents only when expanded. */ -function AllMessagesBody({uri, messages}: {uri: DocumentUri, messages: () => Promise}) { +function AllMessagesBody({uri, curPos, messages}: {uri: DocumentUri, curPos: DocumentPosition | undefined , messages: () => Promise}) { const [msgs, setMsgs] = React.useState(undefined) - React.useEffect(() => { void messages().then(setMsgs) }, [messages]) + React.useEffect(() => { void messages().then( + msgs => setMsgs(msgs.filter( + (d)=>{ + //console.log(`message start: ${d.range.start.line}. CurPos: ${curPos.line}`) + + // Only show the messages from the line where the cursor is. + return d.range.start.line == curPos.line + })) + ) }, [messages, curPos]) if (msgs === undefined) return
Loading messages...
else return } diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index beaf30b..24fc18d 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -73,7 +73,7 @@ function Level() { } -function ChatPanel({lastLevel}) { +function ChatPanel({lastLevel, visible = true}) { const chatRef = useRef(null) const {mobile} = useContext(PreferencesContext) const gameId = useContext(GameIdContext) @@ -122,7 +122,7 @@ function ChatPanel({lastLevel}) { let introText: Array = level?.data?.introduction.split(/\n(\s*\n)+/) - return
+ return
{introText?.filter(t => t.trim()).map(((t, i) => // Show the level's intro text as hints, too @@ -177,7 +177,7 @@ function ChatPanel({lastLevel}) { } -function ExercisePanel({codeviewRef, visible=true}) { +function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject, visible?: boolean}) { const gameId = React.useContext(GameIdContext) const {worldId, levelId} = useContext(WorldLevelIdContext) const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) @@ -602,7 +602,7 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange setInfoProvider(infoProvider) // TODO: it looks like we get errors "File Changed" here. - client.restart() + client.restart("Lean4Game") const editorApi = infoProvider.getApi()