diff --git a/client/src/app.css b/client/src/app.css index df779d6..aa077c0 100644 --- a/client/src/app.css +++ b/client/src/app.css @@ -120,7 +120,8 @@ em { font-weight: 500; font-size: 1.3rem; display: inline-block; - margin: 0 1em; + margin: 0; + /* margin: 0 1em; */ } .app-content { diff --git a/client/src/app.tsx b/client/src/app.tsx index 69afb7d..d4605eb 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -8,16 +8,26 @@ import '@fontsource/roboto/700.css'; import './reset.css'; import './app.css'; +import { MobileContext } from './components/infoview/context'; +import { useWindowDimensions } from './window_width'; export const GameIdContext = React.createContext(undefined); function App() { const params = useParams() const gameId = "g/" + params.owner + "/" + params.repo + + // TODO: Make mobileLayout be changeable in settings + // TODO: Handle resize Events + const {width, height} = useWindowDimensions() + const [mobile, setMobile] = React.useState(width < 800) + return (
- + + +
) diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index 4549e04..2f6c23d 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -60,7 +60,15 @@ export const ProofStateContext = React.createContext<{ termGoal: undefined, error: undefined}, setProofState: () => {}, -}); +}) + +export const MobileContext = React.createContext<{ + mobile : boolean, + setMobile: React.Dispatch> +}>({ + mobile : false, + setMobile: () => {}, +}) /** Context to keep highlight selected proof step and corresponding chat messages. */ export const SelectionContext = React.createContext<{ diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 1c6e83b..1004ec1 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -27,7 +27,7 @@ import Markdown from '../markdown'; import { Infos } from './infos'; import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; import { Goal } from './goals'; -import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './context'; +import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './context'; import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line'; import { InteractiveDiagnostic } from '@leanprover/infoview/*'; import { Button } from '../button'; @@ -38,7 +38,7 @@ import { store } from '../../state/store'; /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is * always present, or the monaco editor cannot start. */ -export function DualEditor({ level, codeviewRef, levelId, worldId }) { +export function DualEditor({ level, codeviewRef, levelId, worldId, lastLevel = false }) { const ec = React.useContext(EditorContext) const { commandLineMode } = React.useContext(InputModeContext) return <> @@ -47,7 +47,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId }) {
{ec ? - : + : // TODO: Style this if relevant. <>

Editor is starting up...

@@ -58,7 +58,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId }) { } /** The part of the two editors that needs the editor connection first */ -function DualEditorMain({ worldId, levelId, level }: { worldId: string, levelId: number, level: LevelInfo }) { +function DualEditorMain({ worldId, levelId, level, lastLevel }: { worldId: string, levelId: number, level: LevelInfo, lastLevel: boolean }) { const ec = React.useContext(EditorContext) const gameId = React.useContext(GameIdContext) const { commandLineMode } = React.useContext(InputModeContext) @@ -108,7 +108,7 @@ function DualEditorMain({ worldId, levelId, level }: { worldId: string, levelId: {commandLineMode ? - + :
} @@ -281,7 +281,7 @@ function GoalsTab({ proofStep }: { proofStep: ProofStep }) { } /** The interface in command line mode */ -export function CommandLineInterface(props: { world: string, level: number, data: LevelInfo }) { +export function CommandLineInterface(props: { world: string, level: number, data: LevelInfo, lastLevel: boolean }) { const ec = React.useContext(EditorContext) const editor = React.useContext(MonacoEditorContext) @@ -290,6 +290,8 @@ export function CommandLineInterface(props: { world: string, level: number, data const { selectedStep, setSelectedStep } = React.useContext(SelectionContext) const { setDeletedChat, showHelp } = React.useContext(DeletedChatContext) + const {mobile} = React.useContext(MobileContext) + const proofPanelRef = React.useRef(null) // React.useEffect(() => { @@ -324,6 +326,7 @@ export function CommandLineInterface(props: { world: string, level: number, data function toggleSelectStep(line: number) { return (ev) => { + if (mobile) {return} if (selectedStep == line) { setSelectedStep(undefined) console.debug(`unselected step`) diff --git a/client/src/components/level.css b/client/src/components/level.css index 83c0f7e..5fd0b15 100644 --- a/client/src/components/level.css +++ b/client/src/components/level.css @@ -5,6 +5,13 @@ display: flex; } +.level-mobile { + height: 100%; + flex: 1; + min-height: 0; + /* display: flex; */ +} + .hidden { display: none; } diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 63c0926..4ff357a 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -39,11 +39,12 @@ import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'; import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited, selectHelp, selectDifficulty, selectInventory } from '../state/progress'; import { DualEditor } from './infoview/main' import { DeletedHint, DeletedHints, Hints } from './hints'; -import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './infoview/context'; +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'; function Level() { @@ -80,6 +81,10 @@ function PlayableLevel({worldId, levelId}) { 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() !== "") @@ -123,7 +128,9 @@ function PlayableLevel({worldId, levelId}) { useEffect(() => { // TODO: For some reason this is always called twice console.debug('scroll chat') - chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0) + if (!mobile) { + chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0) + } }, [proof, showHelp]) React.useEffect(() => { @@ -181,6 +188,8 @@ function PlayableLevel({worldId, levelId}) { } const gameInfo = useGetGameInfoQuery({game: gameId}) + const lastLevel = levelId >= gameInfo.data?.worldSize[worldId] + const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) const dispatch = useAppDispatch() @@ -295,56 +304,13 @@ function PlayableLevel({worldId, levelId}) { - - -
-
- {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 && (levelId >= gameInfo.data?.worldSize[worldId] ? - : - ) - } - {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) && - - } -
-
-
+ + {mobile? +
+
@@ -353,17 +319,78 @@ function PlayableLevel({worldId, levelId}) { {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) && + + } +
+
+
+ + +
+ +
+
+
+ {impressum ? : null} +
+
+ {!level.isLoading && + <>{inventoryDoc ? + + : + + } + } +
+
+ } @@ -413,6 +440,8 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle, toggleImpressum}) const gameId = React.useContext(GameIdContext) const gameInfo = useGetGameInfoQuery({game: gameId}) + const {mobile} = React.useContext(MobileContext) + const difficulty = useSelector(selectDifficulty(gameId)) const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) @@ -421,19 +450,21 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle, toggleImpressum}) const [navOpen, setNavOpen] = React.useState(false) return
-
- - {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`} - -
+ {!mobile && +
+ + {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`} + +
+ }
{levelTitle} -
+
{levelId < gameInfo.data?.worldSize[worldId] &&