phc
/
lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

wip client modifications

Browse Source
pull/118/head
Jon Eugster 3 years ago
parent 8be7f2f17b
commit 30c5648efb
2 changed files with 89 additions and 16 deletions
Show Stats Download Patch File Download Diff File

34
client/src/components/infoview/main.tsx
Unescape Escape View File

@ -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 ?
<CommandLineInterface world={worldId} level={levelId} data={level} worldSize={worldSize}/>
:
<Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />
<Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} data={level}/>
}
</ProgressContext.Provider>
</WithLspDiagnosticsContext>
@ -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))

71
client/src/components/level.tsx
Unescape Escape View File

@ -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() {
<MonacoEditorContext.Provider value={editor}>
<LevelAppBar
isLoading={level.isLoading}
lockEditorMode={level.data?.template !== null}
levelTitle={`${mobile ? '' : 'Level '}${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
(level?.data?.title && ` : ${level?.data?.title}`)}
toggleImpressum={toggleImpressum}
@ -422,7 +454,7 @@ function Introduction() {
}
/** The top-navigation bar */
function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undefined, setPageNumber = undefined}) {
function LevelAppBar({isLoading, levelTitle, toggleImpressum, lockEditorMode=false, pageNumber = undefined, setPageNumber = undefined}) {
const gameId = React.useContext(GameIdContext)
const {worldId, levelId} = useContext(WorldLevelIdContext)
const gameInfo = useGetGameInfoQuery({game: gameId})
@ -436,6 +468,13 @@ function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undef
const [navOpen, setNavOpen] = React.useState(false)
function toggleEditor(ev) {
if (!lockEditorMode){
setCommandLineMode(!commandLineMode)
setNavOpen(false)
}
}
return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
{mobile ?
<>
@ -481,9 +520,9 @@ function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undef
<Button to={`/${gameId}`} inverted="true" title="back to world selection">
<FontAwesomeIcon icon={faHome} />&nbsp;Home
</Button>
<Button disabled={levelId <= 0} inverted="true" to=""
onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
title="toggle Editor mode">
<Button disabled={levelId <= 0 || lockEditorMode} inverted="true" to=""
onClick={(ev) => {toggleEditor(ev)}}
title={lockEditorMode ? "Editor mode is enforced!" : "toggle Editor mode"}>
<FontAwesomeIcon icon={faCode} />&nbsp;Toggle Editor
</Button>
<Button title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
@ -528,9 +567,9 @@ function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undef
<FontAwesomeIcon icon={faHome} />&nbsp;Leave World
</Button>
}
<Button disabled={levelId <= 0} inverted="true" to=""
onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
title="toggle Editor mode">
<Button disabled={levelId <= 0 || lockEditorMode} inverted="true" to=""
onClick={(ev) => { toggleEditor(ev) }}
title={lockEditorMode ? "Editor mode is enforced!" : "toggle Editor mode"}>
<FontAwesomeIcon icon={faCode} />
</Button>
<Button title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
@ -670,6 +709,7 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
function useLoadWorldFiles(worldId) {
const gameId = React.useContext(GameIdContext)
const gameInfo = useGetGameInfoQuery({game: gameId})
// const templates = useGetTemplateQuery({game: gameId, world: worldId})
const store = useStore()
useEffect(() => {
@ -681,8 +721,17 @@ function useLoadWorldFiles(worldId) {
if (model) {
models.push(model)
} else {
const code = selectCode(gameId, worldId, levelId)(store.getState())
models.push(monaco.editor.createModel(code, 'lean4', uri))
// 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))
}
}
return () => { for (let model of models) { model.dispose() } }

Write Preview
Loading…
Cancel
Save