diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index a4591f6..8d7da75 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -21,13 +21,13 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { GameIdContext } from '../../app'; import { useAppDispatch, useAppSelector } from '../../hooks'; import { LevelInfo } from '../../state/api'; -import { changedInventory, levelCompleted, selectCompleted, selectInventory } from '../../state/progress'; +import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress'; import Markdown from '../markdown'; import { Infos } from './infos'; import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; import { Goal } from './goals'; -import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './context'; +import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context'; import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line'; import { InteractiveDiagnostic } from '@leanprover/infoview/*'; import { Button } from '../button'; @@ -70,7 +70,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin '$/game/completed', (params: any) => { if (ec.events.changedCursorLocation.current && - ec.events.changedCursorLocation.current.uri === params.uri) { + ec.events.changedCursorLocation.current.uri === params.uri) { dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId })) // On completion, add the names of all new items to the local storage @@ -111,7 +111,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin {commandLineMode ? : -
+
} @@ -136,9 +136,33 @@ function ExerciseStatement({ data }) { // TODO: This is only used in `EditorInterface` // while `CommandLineInterface` has this copy-pasted in. -export function Main(props: { world: string, level: number }) { +export function Main(props: { world: string, level: number, data: LevelInfo}) { const ec = React.useContext(EditorContext); const gameId = React.useContext(GameIdContext) + const {worldId, levelId} = React.useContext(WorldLevelIdContext) + + + console.debug(`template: ${props.data.template}`) + + React.useEffect (() => { + if (props.data.template) { + let code: string = selectCode(gameId, worldId, levelId)(store.getState()) + if (!code.length) { + //models.push(monaco.editor.createModel(code, 'lean4', uri)) + } + } + }, [props.data.template]) + // let code: string = selectCode(gameId, worldId, levelId)(store.getState()) + // if (!code.length) { + // console.debug("template: yaay") + // // const template = templates.data[levelId-1] + // if (template) { + // code = templates.data[levelId-1] + // } + // } else { + // console.debug(`template? naah: ${code}`) + // } + // models.push(monaco.editor.createModel(code, 'lean4', uri)) const completed = useAppSelector(selectCompleted(gameId, props.world, props.level)) diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 074154b..2e95be5 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -227,8 +227,6 @@ function PlayableLevel() { const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null) function closeInventoryDoc () {setInventoryDoc(null)} - - const onDidChangeContent = (code) => { dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code})) } @@ -244,6 +242,39 @@ function PlayableLevel() { const {editor, infoProvider, editorConnection} = useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) +// const editor = React.useContext(MonacoEditorContext) +// // let code = selectCode(gameId, worldId, levelId)(store.getState()) +// // if (commandLineMode && !code?.length) { +// // console.debug(`inserting template: ${template}`) +// // editor.executeEdits("command-line", [{ +// // range: editor.getModel().getFullModelRange(), +// // text: "hallo" +// // }]) +// // console.debug('inserted template') +// // //dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code: template})) +// // } + + useEffect (() => { + // Lock editor mode + if (level?.data?.template) { + setCommandLineMode(false) + console.debug(`inserting template: ${level.data.template}`) + + // TODO: This does not work! HERE + // Probably overwritten by a query to the server + editor.executeEdits("command-line", [{ + range: editor.getModel().getFullModelRange(), + text: level.data.template, + forceMoveMarkers: false + }]) + + } else { + setCommandLineMode(true) + } + + + }, [level, levelId, worldId, gameId]) + /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside * `CommandLineInterface`. */ @@ -347,6 +378,7 @@ function PlayableLevel() { {mobile ? <> @@ -481,9 +520,9 @@ function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undef - } -