- {(!worldId || !levelId) &&
+ {/* { ((mobile && !worldId) || worldId && !levelId) &&
// Start button appears only on world selection and level 0.
+ } */}
+ {!levelId && (readIntro || (counter >= introMessages.length) ?
+ ((worldId || mobile) &&
+ <>
+
+}
+
+/** Insert the variable names in a hint. We do this client-side to prepare
+ * for i18n in the future. i.e. one should be able translate the `rawText`
+ * and have the variables substituted just before displaying.
+ */
+function getHintText(hint: GameHint): string {
+ const {gameId} = React.useContext(GameIdContext)
+ let { t } = useTranslation()
+ if (hint.rawText) {
+ // Replace the variable names used in the hint with the ones used by the player
+ // variable names are marked like `«{g}»` inside the text.
+ return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
+ // `hint.varNames` contains tuples `[oldName, newName]`
+ (hint.varNames.find(x => x[0] == v))[1]))
+ } else {
+ // hints created in the frontend do not have a `rawText`
+ // TODO: `hint.text` could be removed in theory.
+ return t(hint.text, {ns: gameId})
+ }
+}
+
+/** Bundling a hint with the proof-step it comes from. */
+type GameHintWithStep = {
+ hint: GameHint
+ step?: number
+ conclusion?: boolean
+}
+
+/** Filter hints to not show consequtive identical hints twice.
+ * Hidden hints are not filtered.
+ */
+export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
+ if (!hints) {
+ return []
+ } else if (!prevHints) {
+ return [...hints.filter((hint) => !hint.hidden), ...hints.filter((hint) => hint.hidden)]
+ } else {
+ return [...hints.filter((hint) => !hint.hidden &&
+ (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
+ ), ...hints.filter((hint) => hint.hidden)]
+ }
+}
+
+/** A hint as it is displayed in the chat. */
+export function Hint({hint, step=null, conclusion=false} : GameHintWithStep) {
+ const { levelId } = useContext(GameIdContext)
+ const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = useContext(ChatContext)
+
+ const { proof } = useContext(ProofContext)
+ const { typewriterMode } = useContext(PageContext)
+
+ function toggleSelection () {
+ if (!levelId) {return}
+
+ if (selectedStep !== null && selectedStep == step) {
+ setSelectedStep(undefined)
+ } else if (step < proof?.steps?.length) {
+ setSelectedStep(step)
}
+ }
+
+ // "Deleted hints" are marked in grey. They are used two-fold:
+ // In typewriter, deleting parts of the proof stores the removed hints as `deletedChat`
+ // until the next command is submitted; in editor, moving the cursor through the proof will
+ // render all hints
+ return = (typewriterMode ? proof?.steps?.length : selectedStep+1) ? ' deleted-hint' : '') } onClick={toggleSelection}>
+ {getHintText(hint)}
}
+/** A collection of hints. If the `counter` is defined, only the first elements will be
+ * shown up to the value of the `counter`.
+ *
+ * Set `conclusion` to true to trigger different style and disable selecting/deleting.
+ */
+export function Hints({ hints, conclusion, counter=undefined } : {
+ hints: GameHintWithStep[],
+ conclusion?: boolean,
+ counter?: number
+}) {
+
+ const { showHelp } = useContext(ChatContext)
+
+ if (!hints) {
+ return <>
+ }
+
+ // NOTE: This builds on the fact that `.slice(0, undefined)` returns the whole array!
+ // TODO: Should not use index as key.
+ return <>
+ { hints.slice(0, counter).map((hint, j) =>
+ ((!hint.hint.hidden || showHelp.has(hint.step)) &&
+
- (null)
-
const { gameId, worldId, levelId } = React.useContext(GameIdContext)
// Load the namespace of the game
i18next.loadNamespaces(gameId)
- const {mobile} = React.useContext(PreferencesContext)
+ const {mobile} = useContext(PreferencesContext)
const {isSavePreferences, language, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
const gameInfo = useGetGameInfoQuery({game: gameId})
@@ -48,21 +48,35 @@ function Game() {
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
+ const {page, setPage} = useContext(PageContext)
+
+ // TODO: recover `readIntro` functionality
+
+ // const [pageNumber, setPageNumber] = React.useState(readIntro ? 1 : 0)
+
+ // 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())
+ // 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(null)
- const {page, setPage} = React.useContext(PageContext)
+ // The state variables for the `ProofContext`
+ const [proof, setProof] = useState({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
+ const [interimDiags, setInterimDiags] = useState>([])
+ const [isCrashed, setIsCrashed] = useState(false)
- // TODO: recover `openedIntro` functionality
- // const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
+ const dispatch = useAppDispatch()
- // pop-ups
- const [eraseMenu, setEraseMenu] = React.useState(false)
- const [impressum, setImpressum] = React.useState(false)
- const [privacy, setPrivacy] = React.useState(false)
- const [info, setInfo] = React.useState(false)
- const [rulesHelp, setRulesHelp] = React.useState(false)
- const [uploadMenu, setUploadMenu] = React.useState(false)
- const [preferencesPopup, setPreferencesPopup] = React.useState(false)
+ const typewriterMode = useSelector(selectTypewriterMode(gameId))
+ const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
+
+ const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
+ const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
// set the window title
useEffect(() => {
@@ -71,27 +85,40 @@ function Game() {
}
}, [gameInfo.data?.title])
- return mobile ?
-
+ */}
}
@@ -403,23 +402,21 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number
export function TypewriterInterface({props}) {
let { t } = useTranslation()
const ec = React.useContext(EditorContext)
- const {gameId} = React.useContext(GameIdContext)
+ const {gameId,worldId, levelId} = React.useContext(GameIdContext)
const editor = React.useContext(MonacoEditorContext)
const model = editor.getModel()
const uri = model.uri.toString()
const gameInfo = useGetGameInfoQuery({game: gameId})
- const {worldId, levelId} = React.useContext(WorldLevelIdContext)
let image: string = gameInfo.data?.worlds.nodes[worldId].image
const [disableInput, setDisableInput] = React.useState
+ }
}
diff --git a/client/src/components/editor.tsx b/client/src/components/editor.tsx
new file mode 100644
index 0000000..ee5ace7
--- /dev/null
+++ b/client/src/components/editor.tsx
@@ -0,0 +1,7 @@
+import * as React from 'react'
+
+export function Editor () {
+ return
+
+ {/* {proof?.steps.map((step, i) =>
+ ({hint: hint, step: i}))}/>
+ )} */}
+ {/* ({hint: hint, step: proof?.steps?.length - 1}))} /> */}
+
+ { deletedChat &&
+ ({hint: hint, step: proof?.steps?.length}))} />
+ }
+ { completed && levelInfo.data?.conclusion &&
+
- { mobile && + I'm an editor +
+} diff --git a/client/src/components/game.tsx b/client/src/components/game.tsx index 45a2b31..75e6d5a 100644 --- a/client/src/components/game.tsx +++ b/client/src/components/game.tsx @@ -1,5 +1,5 @@ import * as React from 'react' -import { useEffect, useRef } from 'react' +import { useContext, useEffect, useRef, useState } from 'react' import Split from 'react-split' import { Box, CircularProgress } from '@mui/material' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' @@ -7,10 +7,10 @@ import { faArrowRight } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from '../app' import { useAppDispatch, useAppSelector } from '../hooks' -import { changedOpenedIntro, selectOpenedIntro } from '../state/progress' +import { changeTypewriterMode, changedReadIntro, changedSelection, codeEdited, selectCode, selectReadIntro, selectSelections, selectTypewriterMode } from '../state/progress' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api' import { Button } from './button' -import { PageContext, PreferencesContext } from './infoview/context' +import { ChatContext, PageContext, PreferencesContext, ProofContext } from './infoview/context' import { InventoryPanel } from './inventory' import { ErasePopup } from './popup/erase' import { InfoPopup } from './popup/info' @@ -22,25 +22,25 @@ import { WorldTreePanel } from './world_tree' import '../css/game.css' import '../css/welcome.css' import '../css/level.css' -import { Hint } from './hints' import i18next from 'i18next' import { useTranslation } from 'react-i18next' import { LoadingIcon } from './utils' import { ChatPanel } from './chat' import { DualEditor } from './infoview/main' -import { Level } from './level' +import { Level, LevelWrapper } from './level' +import { GameHint, ProofState } from './infoview/rpc_api' +import { useSelector } from 'react-redux' +import { Diagnostic } from 'vscode-languageserver-types' /** main page of the game showing among others the tree of worlds/levels */ function Game() { - const codeviewRef = useRef
- {<>
- 0 && page == 1} /> :
-
+
+ { mobile ?
+
-
+ :
+
+
+ }
+
+
}
diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx
deleted file mode 100644
index 257e521..0000000
--- a/client/src/components/hints.tsx
+++ /dev/null
@@ -1,125 +0,0 @@
-import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api";
-import * as React from 'react';
-import Markdown from './markdown';
-import { DeletedChatContext, ProofContext } from "./infoview/context";
-import { lastStepHasErrors } from "./infoview/goals";
-import { Button } from "./button";
-import { useTranslation } from "react-i18next";
-import { GameIdContext } from "../app";
-
-/** Plug-in the variable names in a hint. We do this client-side to prepare
- * for i18n in the future. i.e. one should be able translate the `rawText`
- * and have the variables substituted just before displaying.
- */
-function getHintText(hint: GameHint): string {
- const {gameId} = React.useContext(GameIdContext)
- let { t } = useTranslation()
- if (hint.rawText) {
- // Replace the variable names used in the hint with the ones used by the player
- // variable names are marked like `«{g}»` inside the text.
- return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
- // `hint.varNames` contains tuples `[oldName, newName]`
- (hint.varNames.find(x => x[0] == v))[1]))
- } else {
- // hints created in the frontend do not have a `rawText`
- // TODO: `hint.text` could be removed in theory.
- return t(hint.text, {ns: gameId})
- }
-}
-
-export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
- return )}
-
-}
-
-/** Filter hints to not show consequtive identical hints twice.
- * Hidden hints are not filtered.
- */
-export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
- if (!hints) {
- return []}
- else if (!prevHints) {
- return hints }
- else {
- return hints.filter((hint) => hint.hidden ||
- (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
- )
- }
-}
-
-
-function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
- return step?.goals[0]?.hints.some((hint) => hint.hidden)
-}
-
-
-export function MoreHelpButton({selected=null} : {selected?: number}) {
-
- const { t } = useTranslation()
-
- const {proof, setProof} = React.useContext(ProofContext)
- const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
-
- let k = proof?.steps.length ?
- ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
- : 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?.steps.length)) {return}
-
- // state must not be mutated, therefore we need to clone the set
- let tmp = new Set(showHelp)
- if (tmp.has(k)) {
- tmp.delete(k)
- } else {
- tmp.add(k)
- }
- setShowHelp(tmp)
- console.debug(`help: ${Array.from(tmp.values())}`)
- }
-
- if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
- return
- }
-}
diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts
index 363d5c9..afa5d5d 100644
--- a/client/src/components/infoview/context.ts
+++ b/client/src/components/infoview/context.ts
@@ -93,30 +93,17 @@ export const PreferencesContext = React.createContext({
setLanguage: () => {},
})
-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<{
+export const ChatContext = React.createContext<{
selectedStep : number,
setSelectedStep: React.Dispatch>
-}>({
- selectedStep : undefined,
- setSelectedStep: () => {}
-})
-
-/** Context for deleted Hints that are visible just a bit after they've been deleted */
-export const DeletedChatContext = React.createContext<{
deletedChat : GameHint[],
setDeletedChat: React.Dispatch>>
showHelp : Set,
setShowHelp: React.Dispatch>>
}>({
+ selectedStep : undefined,
+ setSelectedStep: () => {},
deletedChat: undefined,
setDeletedChat: () => {},
showHelp: undefined,
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index 5d1bc79..a4cb524 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -20,25 +20,26 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
import { GameIdContext } from '../../app';
import { useAppDispatch, useAppSelector } from '../../hooks';
-import { LevelInfo, useGetGameInfoQuery } from '../../state/api';
+import { LevelInfo, useGetGameInfoQuery, useLoadLevelQuery } from '../../state/api';
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, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals';
-import { DeletedChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context';
+import { ChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext } from './context';
import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter';
import { InteractiveDiagnostic } from '@leanprover/infoview/*';
import { Button } from '../button';
import { CircularProgress } from '@mui/material';
import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
import { store } from '../../state/store';
-import { Hints, MoreHelpButton, filterHints } from '../hints';
import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
import { DiagnosticSeverity } from 'vscode-languageclient';
import { useTranslation } from 'react-i18next';
import path from 'path';
+import { useContext } from 'react';
+import { Hints, MoreHelpButton, filterHints } from '../chat';
/** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
@@ -49,7 +50,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize })
const { typewriterMode, lockEditorMode } = React.useContext(PageContext)
return <>
}
+ {<>
+
- :
-
- {/* Note: apparently without this `div` the split panel bugs out. */}
- {worldId ?
-
+ {/* Note: apparently without this `div` the split panel bugs out. */}
+ {worldId ? (levelId > 0 &&
+
- {getHintText(hint)}
-
-}
-
-export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
- return
- {getHintText(hint)}
-
-}
-
-export function Hints({hints, showHidden, step, selected, toggleSelection, lastLevel} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
- if (!hints) {return <>}
- const openHints = hints.filter(hint => !hint.hidden)
- const hiddenHints = hints.filter(hint => hint.hidden)
-
- // TODO: Should not use index as key.
- return <>
- {openHints.map((hint, j) =>
- {getHintText(hint)}
-
-}
-
-export function DeletedHints({hints} : {hints: GameHint[]}) {
-
- const openHints = hints.filter(hint => !hint.hidden)
- const hiddenHints = hints.filter(hint => hint.hidden)
-
- // TODO: Should not use index as key.
- return <>
- {openHints.map((hint, i) =>
-
{ec ?
@@ -135,23 +136,24 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
*
* If `showLeanStatement` is true, it will additionally display the lean code.
*/
-function ExerciseStatement({ data, showLeanStatement = false }) {
+export function ExerciseStatement({ showLeanStatement = false }) {
let { t } = useTranslation()
- const {gameId} = React.useContext(GameIdContext)
+ const {gameId, worldId, levelId } = React.useContext(GameIdContext)
+ const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
- if (!(data?.descrText || data?.descrFormat)) { return <> }
+ if (!(levelInfo.data?.descrText || levelInfo.data?.descrFormat)) { return <> }
return <>
- {data?.descrText ?
+ {levelInfo.data?.descrText ?
- {(data?.displayName ? `**${t("Theorem")}** \`${data?.displayName}\`: ` : '') + t(data?.descrText, {ns: gameId})}
- : data?.displayName &&
+ {(levelInfo.data?.displayName ? `**${t("Theorem")}** \`${levelInfo.data?.displayName}\`: ` : '') + t(levelInfo.data?.descrText, {ns: gameId})}
+ : levelInfo.data?.displayName &&
- {`**${t("Theorem")}** \`${data?.displayName}\``}
+ {`**${t("Theorem")}** \`${levelInfo.data?.displayName}\``}
}
- {data?.descrFormat && showLeanStatement &&
-
@@ -162,13 +164,10 @@ function ExerciseStatement({ data, showLeanStatement = false }) {
export function Main(props: { world: string, level: number, data: LevelInfo}) {
let { t } = useTranslation()
const ec = React.useContext(EditorContext);
- const {gameId} = React.useContext(GameIdContext)
- const {worldId, levelId} = React.useContext(WorldLevelIdContext)
+ const {gameId, worldId, levelId} = React.useContext(GameIdContext)
const { proof, setProof } = React.useContext(ProofContext)
- const {selectedStep, setSelectedStep} = React.useContext(SelectionContext)
- const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
-
+ const {selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp} = React.useContext(ChatContext)
function toggleSelection(line: number) {
return (ev) => {
@@ -249,11 +248,11 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
{data?.descrFormat}
{levelInfo.data?.descrFormat}
-
+ {/*
*/}
{image &&
![]({path.join("data",)
}
-
-
- {/*
+
+
*/}
+ {/*
+
+
-
*/}
-
-
+ hints={filteredHints.map(hint => ({hint: hint, step: i}))} />
}
{/* setDisableInput(n > 0) : (n) => {}}/> */}
{!(isLastStepWithErrors(proof, i)) &&
diff --git a/client/src/components/infoview/rpc_api.ts b/client/src/components/infoview/rpc_api.ts
index 3a6acba..bf15a1b 100644
--- a/client/src/components/infoview/rpc_api.ts
+++ b/client/src/components/infoview/rpc_api.ts
@@ -50,7 +50,7 @@ export interface GameHint {
text: string;
hidden: boolean;
rawText: string;
- varNames: string[][]; // in Lean: `Array (Name × Name)`
+ varNames?: string[][]; // in Lean: `Array (Name × Name)`
}
export interface InteractiveGoalWithHints {
diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx
index 3488aa6..7269fd0 100644
--- a/client/src/components/infoview/typewriter.tsx
+++ b/client/src/components/infoview/typewriter.tsx
@@ -17,10 +17,11 @@ import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } fro
import { Diagnostic } from 'vscode-languageserver-types';
import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
-import { DeletedChatContext, PageContext, MonacoEditorContext, ProofContext } from './context'
+import { ChatContext, PageContext, MonacoEditorContext, ProofContext } from './context'
import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
import { GameHint, ProofState } from './rpc_api'
import { useTranslation } from 'react-i18next'
+import { GameIdContext } from '../../app'
export interface GameDiagnosticsParams {
uri: DocumentUri;
@@ -81,8 +82,8 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
/** Reference to the hidden multi-line editor */
const editor = React.useContext(MonacoEditorContext)
- const model = editor.getModel()
- const uri = model.uri.toString()
+ const model = editor?.getModel()
+ const uri = model?.uri.toString()
const [oneLineEditor, setOneLineEditor] = useState(null)
const [processing, setProcessing] = useState(false)
@@ -94,8 +95,10 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
// The context storing all information about the current proof
const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext)
+ const {gameId, worldId, levelId} = React.useContext(GameIdContext)
+
// state to store the last batch of deleted messages
- const {setDeletedChat} = React.useContext(DeletedChatContext)
+ const {setDeletedChat} = React.useContext(ChatContext)
const rpcSess = React.useContext(RpcContext)
@@ -106,13 +109,13 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
// TODO: Desired logic is to only reset this after a new *error-free* command has been entered
setDeletedChat([])
- const pos = editor.getPosition()
+ const pos = editor?.getPosition()
if (typewriterInput) {
setProcessing(true)
- editor.executeEdits("typewriter", [{
+ editor?.executeEdits("typewriter", [{
range: monaco.Selection.fromPositions(
pos,
- editor.getModel().getFullModelRange().getEndPosition()
+ editor?.getModel()?.getFullModelRange()?.getEndPosition()
),
text: typewriterInput.trim() + "\n",
forceMoveMarkers: false
@@ -122,7 +125,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
loadGoals(rpcSess, uri, setProof, setCrashed)
}
- editor.setPosition(pos)
+ editor?.setPosition(pos)
}, [typewriterInput, editor])
useEffect(() => {
@@ -133,8 +136,9 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
/* Load proof on start/switching to typewriter */
useEffect(() => {
+ setProof(null)
loadGoals(rpcSess, uri, setProof, setCrashed)
- }, [])
+ }, [gameId, worldId, levelId])
/** If the last step has an error, add the command to the typewriter. */
useEffect(() => {
@@ -157,7 +161,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
// TODO: loadAllGoals()
if (!hasErrors(params.diagnostics)) {
//setTypewriterInput("")
- editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
+ editor?.setPosition(editor?.getModel()?.getFullModelRange()?.getEndPosition())
}
} else {
// console.debug(`expected uri: ${uri}, got: ${params.uri}`)
diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx
index 77cc599..c047bac 100644
--- a/client/src/components/inventory.tsx
+++ b/client/src/components/inventory.tsx
@@ -12,7 +12,6 @@ import { store } from '../state/store';
import { useSelector } from 'react-redux';
import { useTranslation } from 'react-i18next';
import { t } from 'i18next';
-import { WorldLevelIdContext } from './infoview/context';
import { NavButton } from './navigation';
import { LoadingIcon } from './utils';
@@ -37,16 +36,24 @@ const InventoryContext = createContext<{
/**
*/
-function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, recent=false }) {
+function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc } :
+ { item: InventoryTile,
+ name: any,
+ displayName: any,
+ locked: any,
+ disabled: any,
+ newly: any,
+ showDoc: any
+ }) {
const icon = locked ?
{t("Crashed! Go to editor mode and fix your proof! Last server response:")}
{interimDiags.map(diag => { @@ -569,8 +566,7 @@ export function TypewriterInterface({props}) { } {mobile &&
+ return
{icon} {displayName}
{copied ? >([])
const [modifiedItems, setModifiedItems] = useState>([])
- const [recentItems, setRecentItems] = useState>([])
+ const [currentWorldItems, setCurrentWorldItems] = useState>([])
useEffect(() => {
@@ -111,7 +121,8 @@ function InventoryList({ items, tab=null, setTab=()=>{} } :
let _modifiedItems : InventoryTile[] = items?.map(tile => inventory.includes(tile.name) ? {...tile, locked: false} : tile)
setModifiedItems(_modifiedItems)
// Item(s) proved in the preceeding level
- setRecentItems(_modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1))
+ setCurrentWorldItems(_modifiedItems.filter(x => x.world == worldId && x.level < levelId))
+ // setRecentItems(_modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1))
}, [items, inventory])
@@ -120,7 +131,7 @@ function InventoryList({ items, tab=null, setTab=()=>{} } :
{categories.map((cat) => {
let hasNew = modifiedItems.filter(item => item.new && (cat == item.category)).length > 0
- return
x.category).includes(cat) ? ' recent': ''}`}
+ return
}
x.category).includes(cat) ? ' recent': ''}`}
onClick={() => { setTab(cat) }}>{cat}
})}
@@ -134,7 +145,6 @@ function InventoryList({ items, tab=null, setTab=()=>{} } :
showDoc={() => {setDocTile(item)}}
name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false}
disabled={item.disabled}
- recent={recentItems.map(x => x.name).includes(item.name)}
newly={item.new} />
})
}
@@ -155,7 +165,6 @@ export function Inventory () {
/** Helper function to find if a list of tiles comprises any new elements. */
function containsNew(tiles: InventoryTile[]) {
- console.log(tiles)
return tiles?.filter(item => item.new).length > 0
}
diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx
index 42a3649..49410f3 100644
--- a/client/src/components/landing_page.tsx
+++ b/client/src/components/landing_page.tsx
@@ -59,7 +59,7 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
{data.languages.map((lang) => (
-
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 0a61790..c392869 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -4,7 +4,7 @@ import { useSelector, useStore } from 'react-redux'
import Split from 'react-split'
import { useParams } from 'react-router-dom'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faHome, faArrowRight } from '@fortawesome/free-solid-svg-icons'
+import { faHome, faArrowRight, faCode, faTerminal } 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'
@@ -17,6 +17,7 @@ import { EditorContext } from '../../../node_modules/lean4-infoview/src/infoview
import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection'
import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'
import { Diagnostic } from 'vscode-languageserver-types'
+import { DiagnosticSeverity } from 'vscode-languageclient';
import { GameIdContext } from '../app'
import { useAppDispatch, useAppSelector } from '../hooks'
@@ -27,12 +28,13 @@ import { store } from '../state/store'
import { Button } from './button'
import Markdown from './markdown'
import {InventoryPanel} from './inventory'
-import { hasInteractiveErrors } from './infoview/typewriter'
-import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
- ProofContext, SelectionContext, WorldLevelIdContext, PageContext } from './infoview/context'
-import { DualEditor } from './infoview/main'
+import { Editor } from './editor'
+import { Typewriter } from './typewriter'
+import { ChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
+ ProofContext, PageContext } from './infoview/context'
+import { DualEditor, ExerciseStatement } from './infoview/main'
import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints, MoreHelpButton, filterHints } from './hints'
+import { DeletedHints, Hints, MoreHelpButton } from './hints'
import path from 'path';
import '@fontsource/roboto/300.css'
@@ -54,14 +56,14 @@ import { PreferencesPopup } from './popup/preferences'
import { useTranslation } from 'react-i18next'
import i18next from 'i18next'
import { ChatButtons } from './chat'
+import { NavButton } from './navigation'
monacoSetup()
export function Level({visible = true}) {
- // const params = useParams()
- // const levelId = parseInt(params.levelId)
- // const worldId = params.worldId
+ let { t } = useTranslation()
+
const {gameId, worldId, levelId} = React.useContext(GameIdContext)
@@ -71,153 +73,9 @@ export function Level({visible = true}) {
})
const gameInfo = useGetGameInfoQuery({game: gameId})
+ const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
- // pop-ups
- const [impressum, setImpressum] = React.useState(false)
- const [privacy, setPrivacy] = React.useState(false)
- const [info, setInfo] = React.useState(false)
- const [preferencesPopup, setPreferencesPopup] = React.useState(false)
-
- function closeImpressum() {setImpressum(false)}
- function closePrivacy() {setPrivacy(false)}
- function closeInfo() {setInfo(false)}
- function closePreferencesPopup() {setPreferencesPopup(false)}
- function toggleImpressum() {setImpressum(!impressum)}
- function toggleInfo() {setInfo(!info)}
- function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
-
- useEffect(() => {}, [])
-
- return (null)
- const {mobile} = useContext(PreferencesContext)
- 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))
-
- let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
-
- function toggleSelection(line: number) {
- return (ev) => {
- console.debug('toggled selection')
- if (selectedStep == line) {
- setSelectedStep(undefined)
- } else {
- setSelectedStep(line)
- }
- }
- }
-
- 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])
-
- let introText: Array = t(level?.data?.introduction, {ns: gameId}).split(/\n(\s*\n)+/)
-
- return , visible?: boolean}) {
- 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 (null)
- const {gameId} = React.useContext(GameIdContext)
- const {worldId, levelId} = useContext(WorldLevelIdContext)
- const {mobile} = React.useContext(PreferencesContext)
const dispatch = useAppDispatch()
@@ -227,20 +85,9 @@ export function PlayableLevel() {
const typewriterMode = useSelector(selectTypewriterMode(gameId))
const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
- const gameInfo = useGetGameInfoQuery({game: gameId})
- const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
-
- // The state variables for the `ProofContext`
- const [proof, setProof] = useState({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
- const [interimDiags, setInterimDiags] = useState>([])
- const [isCrashed, setIsCrashed] = useState(false)
-
+ const {deletedChat, setDeletedChat,showHelp, setShowHelp} = useContext(ChatContext)
+ const {proof, setProof} = useContext(ProofContext)
- // 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())
// Only for mobile layout
const {page, setPage} = useContext(PageContext)
@@ -259,8 +106,6 @@ export 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}))
}
@@ -309,7 +154,7 @@ export function PlayableLevel() {
useEffect (() => {
// Lock editor mode
- if (level?.data?.template) {
+ if (levelInfo.data?.template) {
setLockEditorMode(true)
if (editor) {
@@ -325,12 +170,12 @@ export function PlayableLevel() {
// TODO: It does seem that the template is always indented by spaces.
// This is a hack, assuming there are exactly two.
if (!code.join('').trim().length) {
- console.debug(`inserting template:\n${level.data.template}`)
+ console.debug(`inserting template:\n${levelInfo.data.template}`)
// TODO: This does not work! HERE
// Probably overwritten by a query to the server
editor.executeEdits("template-writer", [{
range: editor.getModel().getFullModelRange(),
- text: level.data.template + `\n`,
+ text: levelInfo.data.template + `\n`,
forceMoveMarkers: true
}])
} else {
@@ -340,7 +185,7 @@ export function PlayableLevel() {
} else {
setLockEditorMode(false)
}
- }, [level, levelId, worldId, gameId, editor])
+ }, [levelInfo, levelId, worldId, gameId, editor])
useEffect(() => {
@@ -407,104 +252,346 @@ export function PlayableLevel() {
}
}, [editor, typewriterMode, lockEditorMode, onigasmH == null])
- return <>
-
-
-
-
-
-
- {/*
-
-
-
-
-
-
-}
- //
- //
- //
-
-function IntroductionPanel({gameInfo}) {
- let { t } = useTranslation()
- const {gameId} = React.useContext(GameIdContext)
- const {worldId} = useContext(WorldLevelIdContext)
- const {mobile} = React.useContext(PreferencesContext)
-
- let text: Array = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/)
-
- return
-
-
-
-}
-
-function ChatPanel({lastLevel, visible = true}) {
- let { t } = useTranslation()
- const chatRef = useRef
-
-}
-
-
-export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject
- {introText?.filter(t => t.trim()).map(((t, i) =>
- // Show the level's intro text as hints, too
-
- {proof?.completed &&
- <>
-
-
- {t("Level completed! 🎉")}
-
- {level?.data?.conclusion?.trim() &&
-
- {t(level?.data?.conclusion, {ns: gameId})}
-
- }
-
- }
-
- {proof?.completed && (lastLevel ?
- :
- )
- }
-
-
-
-}
-
-export function PlayableLevel() {
- let { t } = useTranslation()
const codeviewRef = useRef
-
-
-
- (null)
+ const proofPanelRef = React.useRef(null)
+
+ // set to true to prevent switching between typewriter and editor
+ const [lockEditorMode, setLockEditorMode] = useState(false)
+ const [typewriterInput, setTypewriterInput] = useState("")
+ const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
+
+ // // impressum pop-up
+ // function toggleImpressum() {setImpressum(!impressum)}
+ // function togglePrivacy() {setPrivacy(!privacy)}
+
+ // 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 toggleImpressum = () => {
- // setImpressum(!impressum)
- // }
- // const togglePrivacy = () => {
- // setPrivacy(!privacy)
- // }
- return <>
- {/* */}
- {gameInfo.isLoading ?
-
- //
- {text?.filter(t => t.trim()).map(((t, i) =>
-
-
+ {/*
+
+ {levelId > 0 &&
+
+
}
-export default Level
-
-/** The site with the introduction text of a world */
-function Introduction() {
+export function LevelWrapper({visible = true}) {
let { t } = useTranslation()
+ const {gameId, worldId, levelId} = React.useContext(GameIdContext)
- const {gameId} = React.useContext(GameIdContext)
- const {mobile} = useContext(PreferencesContext)
+ // Load the namespace of the game
+ i18next.loadNamespaces(gameId).catch(err => {
+ console.warn(`translations for ${gameId} do not exist.`)
+ })
- const inventory = useLoadInventoryOverviewQuery({game: gameId})
- const gameInfo = useGetGameInfoQuery({game: gameId})
+ const { mobile } = useContext(PreferencesContext)
- const {worldId} = useContext(WorldLevelIdContext)
+ const gameInfo = useGetGameInfoQuery({game: gameId})
+ const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
let image: string = gameInfo.data?.worlds.nodes[worldId].image
+ const codeviewRef = useRef
- {image &&
-
- }
+ const dispatch = useAppDispatch()
+
+ const typewriterMode = useSelector(selectTypewriterMode(gameId))
+ const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
+
+ const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
+ const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
+
+
+ const onDidChangeContent = (code) => {
+ dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code}))
+ }
+
+ 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}))
+ }
+
+
+ useEffect(() => {
+ console.info(`Loading Level: ${mobile}`)
+ }, [mobile, gameId, worldId, levelId])
+
+ // const {editor, infoProvider, editorConnection} =
+ // useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection)
+
+
+
+ /** toggle input mode if allowed */
+ function toggleInputMode(ev: React.MouseEvent) {
+ if (!lockEditorMode) {
+ setTypewriterMode(!typewriterMode)
+ console.log('test')
+ }
+ }
+
+ // { typewriterMode ?
+ //
+ return
+//
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+// function ChatPanel({lastLevel, visible = true}) {
+// let { t } = useTranslation()
+// const chatRef = useRef(null)
+// const {mobile} = useContext(PreferencesContext)
+// const {gameId, worldId, levelId} = useContext(GameIdContext)
+// 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))
+
+// let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
+
+// function toggleSelection(line: number) {
+// return (ev) => {
+// console.debug('toggled selection')
+// if (selectedStep == line) {
+// setSelectedStep(undefined)
+// } else {
+// setSelectedStep(line)
+// }
+// }
+// }
+
+// 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])
+
+// let introText: Array = t(level?.data?.introduction, {ns: gameId}).split(/\n(\s*\n)+/)
+
+// return , visible?: boolean}) {
+ const {gameId, worldId, levelId} = React.useContext(GameIdContext)
+ const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
+ const gameInfo = useGetGameInfoQuery({game: gameId})
+ return
+ //
+ //
+
+// function IntroductionPanel({gameInfo}) {
+// let { t } = useTranslation()
+// const {gameId, worldId} = React.useContext(GameIdContext)
+// const {mobile} = React.useContext(PreferencesContext)
+
+// let text: Array = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/)
+
+// return */}
+// {gameInfo.isLoading ?
+//
+// //
+// }
+
+//
+// }
+
// {mobile?
// // TODO: This is copied from the `Split` component below...
// <>
@@ -530,8 +617,7 @@ function Introduction() {
function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
- const {gameId} = React.useContext(GameIdContext)
- const {worldId, levelId} = useContext(WorldLevelIdContext)
+ const {gameId, worldId, levelId} = React.useContext(GameIdContext)
const [editor, setEditor] = useState(null)
const [infoProvider, setInfoProvider] = useState(null)
@@ -544,6 +630,9 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
const difficulty: number = useSelector(selectDifficulty(gameId))
useEffect(() => {
+ // monaco.editor.getModels().forEach(model => model.dispose());
+
+ console.info(`trying to create model: ${gameId} ${worldId} ${levelId} ${uri}`)
const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
if (onDidChangeContent) {
model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
diff --git a/client/src/components/navigation.tsx b/client/src/components/navigation.tsx
index 522b74b..0cf3832 100644
--- a/client/src/components/navigation.tsx
+++ b/client/src/components/navigation.tsx
@@ -12,7 +12,7 @@ import { useTranslation } from 'react-i18next'
import '../css/navigation.css'
import { PopupContext } from './popup/popup'
import { useSelector } from 'react-redux'
-import { selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
+import { selectCompleted, selectDifficulty, selectProgress, selectReadIntro } from '../state/progress'
import lean4gameConfig from '../config.json'
import { Flag } from './flag'
import { useAppSelector } from '../hooks'
@@ -34,8 +34,9 @@ export const NavButton: React.FC<{
href?: string
inverted?: boolean
disabled?: boolean
-}> = ({icon, iconElement, text, onClick=()=>{}, title, href=null, inverted=false, disabled=false}) => {
- return
+ className?: string
+}> = ({icon, iconElement, text, onClick=()=>{}, title, href=null, inverted=false, disabled=false, className=''}) => {
+ return
{iconElement ?? (icon && setPage(page+1)}
+ disabled={!readIntro}
inverted={true} />
}
@@ -123,13 +128,7 @@ function DesktopNavigationLevel () {
const difficulty = useSelector(selectDifficulty(gameId))
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
- /** toggle input mode if allowed */
- function toggleInputMode(ev: React.MouseEvent) {
- if (!lockEditorMode) {
- setTypewriterMode(!typewriterMode)
- console.log('test')
- }
- }
+ const readIntro = useSelector(selectReadIntro(gameId, worldId))
const worldTitle = gameInfo.data?.worlds.nodes[worldId]?.title
const levelTitle = ((levelId == 0) ?
@@ -166,22 +165,14 @@ function DesktopNavigationLevel () {
icon={faHome}
text={t("Leave World")}
inverted={true}
- disabled={difficulty == 0 || !completed}
+ disabled={levelId > 0 && difficulty == 2 && !completed}
href={`#/${gameId}`} /> :
toggleInputMode(ev)}
- title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} />
- }
}
@@ -228,6 +219,8 @@ export function Navigation () {
const difficulty = useSelector(selectDifficulty(gameId))
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
+ const readIntro = useSelector(selectReadIntro(gameId, worldId))
+
const [navOpen, setNavOpen] = useState(false)
const [langNavOpen, setLangNavOpen] = useState(false)
function toggleNav () {setNavOpen(!navOpen); setLangNavOpen(false)}
@@ -280,6 +273,7 @@ export function Navigation () {
// Show all languages the game is available in
gameInfo.data?.tile?.languages.map(iso =>
+ { image &&
+
+}
+
+//
+
+
+ }
+ { levelId > 0 &&
+
+ toggleInputMode(ev)}
+ title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} />
+
+
}
-
+
+
- // {/*
+//
+// }
+
+
+export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject
+// {introText?.filter(t => t.trim()).map(((t, i) =>
+// // Show the level's intro text as hints, too
+//
+// {proof?.completed &&
+// <>
+//
+//
+// {t("Level completed! 🎉")}
+//
+// {level?.data?.conclusion?.trim() &&
+//
+// {t(level?.data?.conclusion, {ns: gameId})}
+//
+// }
+//
+// }
+//
+// {proof?.completed && (lastLevel ?
+// :
+// )
+// }
+//
+//
+
}
+
+ //
+
+
+
+//
+// }
+
+// /** The site with the introduction text of a world */
+// function Introduction() {
+// let { t } = useTranslation()
+
+// const {gameId, worldId} = React.useContext(GameIdContext)
+// const {mobile} = useContext(PreferencesContext)
+
+// const inventory = useLoadInventoryOverviewQuery({game: gameId})
+
+// const gameInfo = useGetGameInfoQuery({game: gameId})
+
+
+// let image: string = gameInfo.data?.worlds.nodes[worldId].image
+
+
+// // const toggleImpressum = () => {
+// // setImpressum(!impressum)
+// // }
+// // const togglePrivacy = () => {
+// // setPrivacy(!privacy)
+// // }
+// return <>
+// {/*
+// {text?.filter(t => t.trim()).map(((t, i) =>
+//
+//
+// {image &&
+//
+// }
+
+//
+// // {/*
-
diff --git a/client/src/components/typewriter.tsx b/client/src/components/typewriter.tsx
new file mode 100644
index 0000000..5df949e
--- /dev/null
+++ b/client/src/components/typewriter.tsx
@@ -0,0 +1,7 @@
+import * as React from 'react'
+
+export function Typewriter () {
+ return + I'm a typewriter +
+} diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx index 84bcb9e..fb6a80e 100644 --- a/client/src/components/welcome.tsx +++ b/client/src/components/welcome.tsx @@ -7,7 +7,7 @@ import { faArrowRight } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from '../app' import { useAppDispatch, useAppSelector } from '../hooks' -import { changedOpenedIntro, selectOpenedIntro } from '../state/progress' +import { changedReadIntro, selectReadIntro } from '../state/progress' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api' import { Button } from './button' import { PageContext, PreferencesContext } from './infoview/context' @@ -55,7 +55,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, @@ -66,7 +66,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, /** main page of the game showing among others the tree of worlds/levels */ function Welcome() { - const {gameId} = React.useContext(GameIdContext) + const {gameId, worldId} = React.useContext(GameIdContext) // Load the namespace of the game i18next.loadNamespaces(gameId) @@ -78,13 +78,13 @@ function Welcome() { const inventory = useLoadInventoryOverviewQuery({game: gameId}) // For mobile only - const openedIntro = useAppSelector(selectOpenedIntro(gameId)) + const readIntro = useAppSelector(selectReadIntro(gameId, worldId)) const {page, setPage} = React.useContext(PageContext) - // TODO: recover `openedIntro` functionality + // TODO: recover `readIntro` functionality - // const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0) + // const [pageNumber, setPageNumber] = React.useState(readIntro ? 1 : 0) // pop-ups const [eraseMenu, setEraseMenu] = React.useState(false) diff --git a/client/src/components/world_tree.tsx b/client/src/components/world_tree.tsx index 636a1a6..f4d6361 100644 --- a/client/src/components/world_tree.tsx +++ b/client/src/components/world_tree.tsx @@ -197,47 +197,6 @@ export const downloadFile = ({ data, fileName, fileType } : a.remove() } -/** The menu that is shown next to the world selection graph */ -export function WorldSelectionMenu({rulesHelp, setRulesHelp}) { - const { t, i18n } = useTranslation() - const {gameId} = React.useContext(GameIdContext) - const difficulty = useSelector(selectDifficulty(gameId)) - const dispatch = useAppDispatch() - const { mobile } = React.useContext(PreferencesContext) - - - function label(x : number) { - return x == 0 ? t("none") : x == 1 ? t("relaxed") : t("regular") - } - - - return -} - export function computeWorldLayout(worlds) { let elements = [] for (let id in worlds.nodes) { @@ -360,7 +319,7 @@ export function WorldTreePanel ({visible = true}) { let dx = bounds ? s*(bounds.x2 - bounds.x1) + 2*padding : null - return
+ return
{/*