diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 7f4437b..442037d 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -22,7 +22,7 @@ import './level.css' import { Button } from './Button' import { ConnectionContext, useLeanClient } from '../connection'; import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'; -import { codeEdited, selectCode, progressSlice, selectCompleted } from '../state/progress'; +import { changedSelection, codeEdited, selectCode, selectSelections, progressSlice, selectCompleted } from '../state/progress'; import { useAppDispatch, useAppSelector } from '../hooks'; import { useStore } from 'react-redux'; @@ -76,6 +76,7 @@ function PlayableLevel({worldId, levelId}) { const introductionPanelRef = useRef(null) const initialCode = useAppSelector(selectCode(worldId, levelId)) + const initialSelections = useAppSelector(selectSelections(worldId, levelId)) const [commandLineMode, setCommandLineMode] = useState(true) const [commandLineInput, setCommandLineInput] = useState("") @@ -86,6 +87,8 @@ function PlayableLevel({worldId, levelId}) { useEffect(() => { // Scroll to top when loading a new level introductionPanelRef.current!.scrollTo(0,0) + // Reset command line input when loading a new level + setCommandLineInput("") }, [levelId]) React.useEffect(() => { @@ -122,8 +125,6 @@ function PlayableLevel({worldId, levelId}) { }]); } - const connection = React.useContext(ConnectionContext) - const gameInfo = useGetGameInfoQuery() const level = useLoadLevelQuery({world: worldId, level: levelId}) @@ -136,10 +137,37 @@ function PlayableLevel({worldId, levelId}) { setCanUndo(code.trim() !== "") } + const onDidChangeSelection = (monacoSelections) => { + const selections = monacoSelections.map( + ({selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}) => + {return {selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}}) + dispatch(changedSelection({world: worldId, level: levelId, selections})) + } + const completed = useAppSelector(selectCompleted(worldId, levelId)) const {editor, infoProvider, editorConnection} = - useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent) + useLevelEditor(worldId, levelId, codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) + + // Effect when command line mode gets enabled + useEffect(() => { + if (editor && commandLineMode) { + let endPos = editor.getModel().getFullModelRange().getEndPosition() + if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") { + editor.executeEdits("command-line", [{ + range: monaco.Selection.fromPositions(endPos, endPos), + text: "\n", + forceMoveMarkers: true + }]); + } + endPos = editor.getModel().getFullModelRange().getEndPosition() + let currPos = editor.getPosition() + if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) { + // This is not a position that would naturally occur from CommandLine, reset: + editor.setSelection(monaco.Selection.fromPositions(endPos, endPos)) + } + } + }, [editor, commandLineMode]) const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null) @@ -249,7 +277,7 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle}) { } -function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCode, onDidChangeContent) { +function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) { const connection = React.useContext(ConnectionContext) @@ -340,8 +368,11 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo model = monaco.editor.createModel(initialCode, 'lean4', uri) } model.onDidChangeContent(() => onDidChangeContent(model.getValue())) + editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections())) editor.setModel(model) - editor.setPosition(model.getFullModelRange().getEndPosition()) + if (initialSelections) { + editor.setSelections(initialSelections) + } infoviewApi.serverRestarted(leanClient.initializeResult) infoProvider.openPreview(editor, infoviewApi) diff --git a/client/src/components/infoview/CommandLine.tsx b/client/src/components/infoview/CommandLine.tsx index b565761..72fa488 100644 --- a/client/src/components/infoview/CommandLine.tsx +++ b/client/src/components/infoview/CommandLine.tsx @@ -170,21 +170,6 @@ export function CommandLine() { return () => { l.dispose() } }, [oneLineEditor, runCommand]) - // Effect when command line mode gets enabled - useEffect(() => { - if (commandLineMode) { - const endPos = editor.getModel().getFullModelRange().getEndPosition() - if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") { - editor.executeEdits("command-line", [{ - range: monaco.Selection.fromPositions(endPos, endPos), - text: commandLineInput + "\n", - forceMoveMarkers: false - }]); - } - editor.setPosition(editor.getModel().getFullModelRange().getEndPosition()) - } - }, [commandLineMode]) - const handleSubmit : React.FormEventHandler = (ev) => { ev.preventDefault() runCommand() diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index dcb0ec7..369bdf7 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -18,7 +18,7 @@ import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '. 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 { codeEdited, levelCompleted, selectCompleted } from '../../state/progress'; +import { levelCompleted, selectCompleted } from '../../state/progress'; export function Main(props: {world: string, level: number}) { diff --git a/client/src/state/progress.ts b/client/src/state/progress.ts index 5512322..6005d4f 100644 --- a/client/src/state/progress.ts +++ b/client/src/state/progress.ts @@ -5,9 +5,15 @@ import { loadState } from "./localStorage"; interface ProgressState { level: {[world: string]: {[level: number]: LevelProgressState}} } - +interface Selection { + selectionStartLineNumber: number, + selectionStartColumn: number, + positionLineNumber: number + positionColumn: number +} interface LevelProgressState { code: string, + selections: Selection[], completed: boolean } @@ -32,6 +38,10 @@ export const progressSlice = createSlice({ state.level[action.payload.world][action.payload.level].code = action.payload.code state.level[action.payload.world][action.payload.level].completed = false }, + changedSelection(state, action: PayloadAction<{world: string, level: number, selections: Selection[]}>) { + addLevelProgress(state, action) + state.level[action.payload.world][action.payload.level].selections = action.payload.selections + }, levelCompleted(state, action: PayloadAction<{world: string, level: number}>) { addLevelProgress(state, action) state.level[action.payload.world][action.payload.level].completed = true @@ -53,6 +63,12 @@ export function selectCode(world: string, level: number) { } } +export function selectSelections(world: string, level: number) { + return (state) => { + return selectLevel(world, level)(state).selections + } +} + export function selectCompleted(world: string, level: number) { return (state) => { return selectLevel(world, level)(state).completed @@ -65,4 +81,4 @@ export function selectProgress() { } } -export const { codeEdited, levelCompleted } = progressSlice.actions +export const { changedSelection, codeEdited, levelCompleted } = progressSlice.actions