diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index 2f6c23d..8f0bce7 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -70,6 +70,14 @@ export const MobileContext = React.createContext<{ setMobile: () => {}, }) +export const WorldLevelIdContext = React.createContext<{ + worldId : string, + levelId: number +}>({ + worldId : null, + levelId: 0, +}) + /** Context to keep highlight selected proof step and corresponding chat messages. */ export const SelectionContext = React.createContext<{ selectedStep : number, diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index f19566f..61b3c75 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -13,7 +13,7 @@ import { useSelector } from 'react-redux'; export function Inventory({levelInfo, openDoc, enableAll=false} : { levelInfo: LevelInfo|InventoryOverview, - openDoc: (name: string, type: string) => void, + openDoc: (props: {name: string, type: string}) => void, enableAll?: boolean, }) { @@ -41,7 +41,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine { items: InventoryTile[], docType: string, - openDoc(name: string, type: string): void, + openDoc(props: {name: string, type: string}): void, defaultTab? : string, level? : LevelInfo|InventoryOverview, enableAll?: boolean, @@ -89,7 +89,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) ).filter(item => ((tab ?? categories[0]) == item.category)).map((item, i) => { return {openDoc(item.name, docType)}} + showDoc={() => {openDoc({name: item.name, type: docType})}} name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false} disabled={item.disabled} newly={item.new} enableAll={enableAll}/> }) @@ -128,24 +128,20 @@ export function Documentation({name, type, handleClose}) { } /** The panel (on the welcome page) showing the user's inventory with tactics, definitions, and lemmas */ -export function InventoryPanel() { +export function InventoryPanel({visible = true}) { const gameId = React.useContext(GameIdContext) const inventory = useLoadInventoryOverviewQuery({game: gameId}) + // The inventory is overlayed by the doc entry of a clicked item const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null) - - // Open the doc of the clicked inventory item - function openInventoryDoc(name: string, type: string) { - setInventoryDoc({name, type}) - } // Set `inventoryDoc` to `null` to close the doc function closeInventoryDoc() {setInventoryDoc(null)} - return
+ return
{inventoryDoc ? : - + }
} diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 5e6379c..a1c573b 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -1,123 +1,288 @@ -import * as React from 'react'; -import { useEffect, useState, useRef } from 'react'; +import * as React from 'react' +import { useEffect, useState, useRef, useContext } from 'react' +import { useSelector, useStore } from 'react-redux' import Split from 'react-split' -import { Alert } from '@mui/material'; -import '@fontsource/roboto/300.css'; -import '@fontsource/roboto/400.css'; -import '@fontsource/roboto/500.css'; -import '@fontsource/roboto/700.css'; -import { InfoviewApi, defaultInfoviewConfig } from '@leanprover/infoview' -import { Link, useParams } from 'react-router-dom'; -import { Box, CircularProgress, FormControlLabel, FormGroup, Switch, IconButton } from '@mui/material'; -import MuiDrawer from '@mui/material/Drawer'; -import Grid from '@mui/material/Unstable_Grid2'; -import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter'; -import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider'; -import 'lean4web/client/src/editor/vscode.css'; -import 'lean4web/client/src/editor/infoview.css'; -import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter'; -import { InfoProvider } from 'lean4web/client/src/editor/infoview'; -import 'lean4web/client/src/editor/infoview.css' -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import './level.css' -import { useSelector, 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 type { Location } from 'vscode-languageserver-protocol'; +import { useParams } from 'react-router-dom' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faBars, faBook, faCode, faPencilSquare, faXmark, faHome, faCircleInfo, faArrowRight, faArrowLeft, faShield, faRotateLeft } from '@fortawesome/free-solid-svg-icons' -import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles'; - -import { GameIdContext } from '../app'; -import { ConnectionContext, connection, useLeanClient } from '../connection'; -import { useAppDispatch, useAppSelector } from '../hooks'; +import { faBars, faBook, faCode, faXmark, faHome, faCircleInfo, faArrowRight, faArrowLeft } from '@fortawesome/free-solid-svg-icons' +import { CircularProgress } from '@mui/material' +import type { Location } from 'vscode-languageserver-protocol' +import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' +import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider' +import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter' +import { InfoProvider } from 'lean4web/client/src/editor/infoview' +import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter' +import { InfoviewApi } from '@leanprover/infoview' +import { EditorContext } 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 { GameIdContext } from '../app' +import { ConnectionContext, connection, useLeanClient } from '../connection' +import { useAppDispatch, useAppSelector } from '../hooks' +import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api' +import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited, + selectHelp, selectDifficulty, selectInventory } from '../state/progress' +import { store } from '../state/store' import { Button } from './button' -import Markdown from './markdown'; -import {Inventory, Documentation} from './inventory'; -import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'; -import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited, selectHelp, selectDifficulty, selectInventory } from '../state/progress'; +import Markdown from './markdown' +import {InventoryPanel} from './inventory' +import { hasInteractiveErrors } from './infoview/command_line' +import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, + ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context' import { DualEditor } from './infoview/main' -import { DeletedHint, DeletedHints, Hints } from './hints'; -import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './infoview/context'; -import { hasInteractiveErrors } from './infoview/command_line'; -import { GameHint } from './infoview/rpc_api'; -import { Impressum } from './privacy_policy'; -import { store } from '../state/store'; -import { useWindowDimensions } from '../window_width'; -import { ArrowLeft } from '@mui/icons-material'; +import { GameHint } from './infoview/rpc_api' +import { DeletedHints, Hints } from './hints' +import { Impressum } from './privacy_policy' + +import '@fontsource/roboto/300.css' +import '@fontsource/roboto/400.css' +import '@fontsource/roboto/500.css' +import '@fontsource/roboto/700.css' +import 'lean4web/client/src/editor/infoview.css' +import 'lean4web/client/src/editor/vscode.css' +import './level.css' function Level() { - - const params = useParams(); + const params = useParams() const levelId = parseInt(params.levelId) const worldId = params.worldId useLoadWorldFiles(worldId) - if (levelId == 0) { - return - } else { - return - } -} + return + {levelId == 0 ? : } + -function PlayableLevel({worldId, levelId}) { - const codeviewRef = useRef(null) +} +function ChatPanel({lastLevel}) { const chatRef = useRef(null) + const {mobile} = useContext(MobileContext) + const gameId = useContext(GameIdContext) + const {worldId, levelId} = useContext(WorldLevelIdContext) + const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + const {proof, setProof} = useContext(ProofContext) + const {deletedChat, setDeletedChat, showHelp, setShowHelp} = useContext(DeletedChatContext) + const {selectedStep, setSelectedStep} = useContext(SelectionContext) + const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) + + // If the last step has errors, we want to treat it as if it is part of the second-to-last step + let k = proof.length - 1 + let withErr = hasInteractiveErrors(proof[k]?.errors) ? 1 : 0 + + function toggleSelection(line: number) { + return (ev) => { + console.debug('toggled selection') + if (selectedStep == line) { + setSelectedStep(undefined) + } else { + setSelectedStep(line) + } + } + } + function hasHiddenHints(i : number): boolean { + let step = proof[i] + // For example if the proof isn't loaded yet + if(!step) {return false} + return step.hints.some((hint) => hint.hidden) + } + + const activateHiddenHints = (ev) => { + // If the last step (`k`) has errors, we want the hidden hints from the + // second-to-last step to be affected + if (!(proof.length)) {return} + + // state must not be mutated, therefore we need to clone the set + let tmp = new Set(showHelp) + if (tmp.has(k - withErr)) { + tmp.delete(k - withErr) + } else { + tmp.add(k - withErr) + } + setShowHelp(tmp) + console.debug(`help: ${Array.from(tmp.values())}`) + } + + + useEffect(() => { + // TODO: For some reason this is always called twice + console.debug('scroll chat') + if (!mobile) { + chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0) + } + }, [proof, showHelp]) + + // Scroll to element if selection changes + useEffect(() => { + if (typeof selectedStep !== 'undefined') { + Array.from(chatRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { + elem.scrollIntoView({block: "center"}) + }) + } + }, [selectedStep]) + + // useEffect(() => { + // // // Scroll to top when loading a new level + // // // TODO: Thats the wrong behaviour probably + // // chatRef.current!.scrollTo(0,0) + // }, [gameId, worldId, levelId]) + + + return
+
+ {level?.data?.introduction && +
+ {level?.data?.introduction} +
+ } + {proof.map((step, i) => { + // It the last step has errors, it will have the same hints + // as the second-to-last step. Therefore we should not display them. + if (!(i == proof.length - 1 && withErr)) { + // TODO: Should not use index as key. + return + } + })} + + {completed && + <> +
+ Level completed! 🎉 +
+ {level?.data?.conclusion?.trim() && +
+ {level?.data?.conclusion} +
+ } + + } +
+
+ {completed && (lastLevel ? + : + ) + } + {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) && + + } +
+
+} + +function ExercisePanel({codeviewRef, impressum, closeImpressum, visible=true}) { const gameId = React.useContext(GameIdContext) + const {worldId, levelId} = useContext(WorldLevelIdContext) + const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + const gameInfo = useGetGameInfoQuery({game: gameId}) + return
+
+ +
+ {impressum ? : null} +
+} + +function PlayableLevel() { + const codeviewRef = useRef(null) + const gameId = React.useContext(GameIdContext) + const {worldId, levelId} = useContext(WorldLevelIdContext) // The state variables for the `ProofContext` const [proof, setProof] = useState>([]) - // When deleting the proof, we want to keep to old messages around until // a new proof has been entered. e.g. to consult messages coming from dead ends const [deletedChat, setDeletedChat] = useState>([]) - // A set of row numbers where help is displayed const [showHelp, setShowHelp] = useState>(new Set()) - const initialCode = useAppSelector(selectCode(gameId, worldId, levelId)) const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId)) - /** Only for mobile layout */ const [pageNumber, setPageNumber] = useState(0) const {mobile} = React.useContext(MobileContext) - const [commandLineMode, setCommandLineMode] = useState(true) const [commandLineInput, setCommandLineInput] = useState("") - const [canUndo, setCanUndo] = useState(initialCode.trim() !== "") + const difficulty = useSelector(selectDifficulty(gameId)) + const inventory: Array = useSelector(selectInventory(gameId)) + const gameInfo = useGetGameInfoQuery({game: gameId}) + const lastLevel = levelId >= gameInfo.data?.worldSize[worldId] + const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + const dispatch = useAppDispatch() - const [selectedStep, setSelectedStep] = useState() + // impressum pop-up + const [impressum, setImpressum] = React.useState(false) + function closeImpressum() {setImpressum(false)} + function toggleImpressum() {setImpressum(!impressum)} - const theme = useTheme(); + // When clicking on an inventory item, the inventory is overlayed by the item's doc. + // If this state is set to a pair `(name, type)` then the according doc will be open. + // Set `inventoryDoc` to `null` to close the doc + const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null) + function closeInventoryDoc () {setInventoryDoc(null)} - const [impressum, setImpressum] = React.useState(false) - const difficulty = useSelector(selectDifficulty(gameId)) - function closeImpressum() { - setImpressum(false) + const onDidChangeContent = (code) => { + dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code})) } - function toggleImpressum() { - setImpressum(!impressum) + const onDidChangeSelection = (monacoSelections) => { + const selections = monacoSelections.map( + ({selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}) => + {return {selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}}) + dispatch(changedSelection({game: gameId, world: worldId, level: levelId, selections})) } - const inventory: Array = useSelector(selectInventory(gameId)) - React.useEffect(() => { + const {editor, infoProvider, editorConnection} = + useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) + + /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside + * `CommandLineInterface`. + */ + const handleUndo = () => { + const endPos = editor.getModel().getFullModelRange().getEndPosition() + let range + console.log(endPos.column) + if (endPos.column === 1) { + range = monaco.Selection.fromPositions( + new monaco.Position(endPos.lineNumber - 1, 1), + endPos + ) + } else { + range = monaco.Selection.fromPositions( + new monaco.Position(endPos.lineNumber, 1), + endPos + ) + } + editor.executeEdits("undo-button", [{ + range, + text: "", + forceMoveMarkers: false + }]); + } + + // Select and highlight proof steps and corresponding hints + // TODO: with the new design, there is no difference between the introduction and + // a hint at the beginning of the proof... + const [selectedStep, setSelectedStep] = useState() + + // if the user inventory changes, notify the server + useEffect(() => { let leanClient = connection.getLeanClient(gameId) leanClient.sendNotification('$/game/setInventory', {inventory: inventory, checkEnabled: difficulty > 0}) }, [inventory]) useEffect(() => { - // // Scroll to top when loading a new level - // // TODO: Thats the wrong behaviour probably - // chatRef.current!.scrollTo(0,0) - // TODO: That's a problem if the saved proof contains an error // Reset command line input when loading a new level setCommandLineInput("") @@ -127,14 +292,6 @@ function PlayableLevel({worldId, levelId}) { }, [gameId, worldId, levelId]) useEffect(() => { - // TODO: For some reason this is always called twice - console.debug('scroll chat') - if (!mobile) { - chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0) - } - }, [proof, showHelp]) - - React.useEffect(() => { if (!commandLineMode) { // Delete last input attempt from command line editor.executeEdits("command-line", [{ @@ -146,16 +303,7 @@ function PlayableLevel({worldId, levelId}) { } }, [commandLineMode]) - // Scroll to element if selection changes - React.useEffect(() => { - if (typeof selectedStep !== 'undefined') { - Array.from(chatRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { - elem.scrollIntoView({block: "center"}) - }) - } - }, [selectedStep]) - - React.useEffect(() => { + useEffect(() => { // Forget whether hidden hints are displayed for steps that don't exist yet if (proof.length) { console.debug(Array.from(showHelp)) @@ -163,44 +311,6 @@ function PlayableLevel({worldId, levelId}) { } }, [proof]) - /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside - * `CommandLineInterface`. - */ - const handleUndo = () => { - const endPos = editor.getModel().getFullModelRange().getEndPosition() - let range - console.log(endPos.column) - if (endPos.column === 1) { - range = monaco.Selection.fromPositions( - new monaco.Position(endPos.lineNumber - 1, 1), - endPos - ) - } else { - range = monaco.Selection.fromPositions( - new monaco.Position(endPos.lineNumber, 1), - endPos - ) - } - editor.executeEdits("undo-button", [{ - range, - text: "", - forceMoveMarkers: false - }]); - } - - const gameInfo = useGetGameInfoQuery({game: gameId}) - const lastLevel = levelId >= gameInfo.data?.worldSize[worldId] - - const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) - - const dispatch = useAppDispatch() - - const onDidChangeContent = (code) => { - dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code})) - - setCanUndo(code.trim() !== "") - } - // save showed help in store useEffect(() => { if (proof.length) { @@ -209,18 +319,6 @@ function PlayableLevel({worldId, levelId}) { } }, [showHelp]) - const onDidChangeSelection = (monacoSelections) => { - const selections = monacoSelections.map( - ({selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}) => - {return {selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}}) - dispatch(changedSelection({game: gameId, world: worldId, level: levelId, selections})) - } - - const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) - - const {editor, infoProvider, editorConnection} = - useLevelEditor(worldId, levelId, codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) - // Effect when command line mode gets enabled useEffect(() => { if (editor && commandLineMode) { @@ -241,173 +339,47 @@ function PlayableLevel({worldId, levelId}) { } }, [editor, commandLineMode]) - // When clicking on an inventory item, the inventory is overlayed by the item's doc. - // If this state is set to a pair `(name, type)` then the according doc will be open. - const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null) - - // Open the doc of the clicked inventory item - function openInventoryDoc(name, type) { - setInventoryDoc({name, type}) - } - - // Set `inventoryDoc` to `null` to close the doc - const closeInventoryDoc = () => setInventoryDoc(null); - - const levelTitle = <> - {levelId && `Level ${levelId} / ${gameInfo.data?.worldSize[worldId]}`}{level?.data?.title && `: ${level?.data?.title}`} - - // TODO: with the new design, there is no difference between the introduction and - // a hint at the beginning of the proof... - - function toggleSelection(line: number) { - return (ev) => { - console.debug('toggled selection') - if (selectedStep == line) { - setSelectedStep(undefined) - } else { - setSelectedStep(line) - } - } - } - - function hasHiddenHints(i : number): boolean { - let step = proof[i] - - // For example if the proof isn't loaded yet - if(!step) {return false} - - return step.hints.some((hint) => hint.hidden) - } - - // If the last step has errors, we want to treat it as if it is part of the second-to-last step - let k = proof.length - 1 - let withErr = hasInteractiveErrors(proof[k]?.errors) ? 1 : 0 - - const activateHiddenHints = (ev) => { - // If the last step (`k`) has errors, we want the hidden hints from the - // second-to-last step to be affected - if (!(proof.length)) {return} - - // state must not be mutated, therefore we need to clone the set - let tmp = new Set(showHelp) - if (tmp.has(k - withErr)) { - tmp.delete(k - withErr) - } else { - tmp.add(k - withErr) - } - setShowHelp(tmp) - console.debug(`help: ${Array.from(tmp.values())}`) - } - return <>
- - - - - {mobile? - // TODO: This is copied from the `Split` component below... - <> -
-
- - -
- -
- - - {impressum ? : null} -
-
-
- {!level.isLoading && - <>{inventoryDoc ? - - : - - } - } -
- - : - -
-
- {level?.data?.introduction && -
- {level?.data?.introduction} -
- } - {proof.map((step, i) => { - // It the last step has errors, it will have the same hints - // as the second-to-last step. Therefore we should not display them. - if (!(i == proof.length - 1 && withErr)) { - // TODO: Should not use index as key. - return - } - })} - - {completed && - <> -
- Level completed! 🎉 -
- {level?.data?.conclusion?.trim() && -
- {level?.data?.conclusion} -
- } - - } -
-
- {completed && (lastLevel ? - : - ) - } - {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) && - - } -
-
-
+ + + -
- -
+ + {mobile? + // TODO: This is copied from the `Split` component below... + <> +
+ + +
+ + : + + + + + + } - {impressum ? : null} -
-
- {!level.isLoading && - <>{inventoryDoc ? - - : - - } - } -
- - } - - - + + + } @@ -415,8 +387,10 @@ function PlayableLevel({worldId, levelId}) { export default Level /** The site with the introduction text of a world */ -function Introduction({worldId}) { +function Introduction() { const gameId = React.useContext(GameIdContext) + const {worldId} = useContext(WorldLevelIdContext) + const gameInfo = useGetGameInfoQuery({game: gameId}) const [impressum, setImpressum] = React.useState(false) @@ -431,7 +405,7 @@ function Introduction({worldId}) { return <>
- +
@@ -450,8 +424,9 @@ function Introduction({worldId}) { } /** The top-navigation bar */ -function LevelAppBar({isLoading, levelId, worldId, levelTitle, toggleImpressum, pageNumber = undefined, setPageNumber = undefined}) { +function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undefined, setPageNumber = undefined}) { const gameId = React.useContext(GameIdContext) + const {worldId, levelId} = useContext(WorldLevelIdContext) const gameInfo = useGetGameInfoQuery({game: gameId}) const {mobile} = React.useContext(MobileContext) @@ -563,10 +538,12 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle, toggleImpressum,
} -function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) { +function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) { const connection = React.useContext(ConnectionContext) const gameId = React.useContext(GameIdContext) + const {worldId, levelId} = useContext(WorldLevelIdContext) + const [editor, setEditor] = useState(null) const [infoProvider, setInfoProvider] = useState(null)