first step towards mobile layout

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 {

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<string>(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 (
     <div className="app">
       <GameIdContext.Provider value={gameId}>
-        <Outlet />
+        <MobileContext.Provider value={{mobile, setMobile}}>
+          <Outlet />
+        </MobileContext.Provider>
       </GameIdContext.Provider>
     </div>
   )

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<React.SetStateAction<Boolean>>
+}>({
+  mobile : false,
+  setMobile: () => {},
+})
 
 /** Context to keep highlight selected proof step and corresponding chat messages. */
 export const SelectionContext = React.createContext<{

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 }) {
       <div ref={codeviewRef} className={'codeview'}></div>
     </div>
     {ec ?
-      <DualEditorMain worldId={worldId} levelId={levelId} level={level} /> :
+      <DualEditorMain worldId={worldId} levelId={levelId} level={level} lastLevel={lastLevel} /> :
       // TODO: Style this if relevant.
       <>
         <p>Editor is starting up...</p>
@@ -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:
           <WithLspDiagnosticsContext>
             <ProgressContext.Provider value={allProgress}>
               {commandLineMode ?
-                <CommandLineInterface world={worldId} level={levelId} data={level} />
+                <CommandLineInterface world={worldId} level={levelId} data={level} lastLevel={lastLevel}/>
                 :
                 <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />
               }
@@ -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<HTMLDivElement>(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`)

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;
 }

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}) {
     <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
     <InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
     <ProofContext.Provider value={{proof, setProof}}>
-      <LevelAppBar isLoading={level.isLoading} levelTitle={`Level ${levelId} / ${gameInfo.data?.worldSize[worldId]}` + (level?.data?.title && ` : ${level?.data?.title}`)} worldId={worldId} levelId={levelId} toggleImpressum={toggleImpressum}/>
+      <LevelAppBar isLoading={level.isLoading}
-      <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
+        levelTitle={`${mobile ? '' : 'Level '}${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
-        <div className="chat-panel">
+          (level?.data?.title && ` : ${level?.data?.title}`)}
-          <div ref={chatRef} className="chat">
+        worldId={worldId} levelId={levelId} toggleImpressum={toggleImpressum}/>
-            {level?.data?.introduction &&
+      {mobile?
-              <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelection(0)}>
+        <div className={`app-content level-mobile ${level.isLoading ? 'hidden' : ''}`}>
-                <Markdown>{level?.data?.introduction}</Markdown>
+          <div className={`exercise-panel ${pageNumber == 0 ? '' : 'hidden'}`}>
-              </div>
-            }
-            {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 <Hints key={`hints-${i}`}
-                  hints={step.hints} showHidden={showHelp.has(i)} step={i}
-                  selected={selectedStep} toggleSelection={toggleSelection(i)}/>
-              }
-            })}
-            <DeletedHints hints={deletedChat}/>
-            {completed &&
-              <>
-                <div className={`message information step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
-                  Level completed! 🎉
-                </div>
-                {level?.data?.conclusion?.trim() &&
-                  <div className={`message information step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
-                    <Markdown>{level?.data?.conclusion}</Markdown>
-                  </div>
-                }
-              </>
-            }
-          </div>
-          <div className="button-row">
-            {completed && (levelId >= gameInfo.data?.worldSize[worldId] ?
-              <Button to={`/${gameId}`}>
-                <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
-              </Button> :
-              <Button to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
-                Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
-              </Button>)
-              }
-            {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-              <Button to="" onClick={activateHiddenHints}>
-                Show more help!
-              </Button>
-            }
-          </div>
-        </div>
-        <div className="exercise-panel">
           <EditorContext.Provider value={editorConnection}>
             <MonacoEditorContext.Provider value={editor}>
               <div className="exercise">
@@ -353,17 +319,78 @@ function PlayableLevel({worldId, levelId}) {
             </MonacoEditorContext.Provider>
           </EditorContext.Provider>
           {impressum ? <Impressum handleClose={closeImpressum} /> : null}
+          </div>
         </div>
-        <div className="inventory-panel">
+      :
-          {!level.isLoading &&
+        <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
-            <>{inventoryDoc ?
+          <div className="chat-panel">
-              <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
+            <div ref={chatRef} className="chat">
-              :
+              {level?.data?.introduction &&
-              <Inventory levelInfo={level?.data} openDoc={openInventoryDoc} />
+                <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelection(0)}>
-            }</>
+                  <Markdown>{level?.data?.introduction}</Markdown>
-          }
+                </div>
-        </div>
+              }
-      </Split>
+              {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 <Hints key={`hints-${i}`}
+                    hints={step.hints} showHidden={showHelp.has(i)} step={i}
+                    selected={selectedStep} toggleSelection={toggleSelection(i)}/>
+                }
+              })}
+              <DeletedHints hints={deletedChat}/>
+              {completed &&
+                <>
+                  <div className={`message information step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
+                    Level completed! 🎉
+                  </div>
+                  {level?.data?.conclusion?.trim() &&
+                    <div className={`message information step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
+                      <Markdown>{level?.data?.conclusion}</Markdown>
+                    </div>
+                  }
+                </>
+              }
+            </div>
+            <div className="button-row">
+              {completed && (lastLevel ?
+                <Button to={`/${gameId}`}>
+                  <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
+                </Button> :
+                <Button to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
+                  Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+                </Button>)
+                }
+              {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+                <Button to="" onClick={activateHiddenHints}>
+                  Show more help!
+                </Button>
+              }
+            </div>
+          </div>
+          <div className="exercise-panel">
+            <EditorContext.Provider value={editorConnection}>
+              <MonacoEditorContext.Provider value={editor}>
+                <div className="exercise">
+                  <DualEditor level={level?.data} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} />
+                </div>
+              </MonacoEditorContext.Provider>
+            </EditorContext.Provider>
+            {impressum ? <Impressum handleClose={closeImpressum} /> : null}
+          </div>
+          <div className="inventory-panel">
+            {!level.isLoading &&
+              <>{inventoryDoc ?
+                <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
+                :
+                <Inventory levelInfo={level?.data} openDoc={openInventoryDoc} />
+              }</>
+            }
+          </div>
+        </Split>
+      }
     </ProofContext.Provider>
     </InputModeContext.Provider>
     </SelectionContext.Provider>
@@ -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 <div className="app-bar" style={isLoading ? {display: "none"} : null} >
-    <div>
+    {!mobile &&
-      <span className="app-bar-title">
+      <div>
-        {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
+        <span className="app-bar-title">
-      </span>
+          {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
-    </div>
+        </span>
+      </div>
+    }
     <div>
       <span className="app-bar-title">
         {levelTitle}
       </span>
-      <Button to="" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}} >
-        {navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
-      </Button>
     </div>
+    <Button to="" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}} >
+      {navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
+    </Button>
     <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
     {levelId < gameInfo.data?.worldSize[worldId] &&
       <Button inverted="true"

client/src/components/welcome.css

@@ -58,7 +58,7 @@ h5, h6 {
 /***************/
 
 svg .world-title-wrapper, svg .level-title-wrapper div {
-  overflow: auto;
+  overflow: visible;
 }
 
 svg .world-title-wrapper div, svg .level-title-wrapper div {

client/src/components/welcome.tsx

@@ -20,6 +20,7 @@ import { Button } from './button';
 import { Documentation, Inventory } from './inventory';
 import { store } from '../state/store';
 import { useWindowDimensions } from '../window_width';
+import { MobileContext } from './infoview/context';
 
 cytoscape.use( klay );
 
@@ -60,18 +61,14 @@ function LevelIcon({ worldId, levelId, position, completed, available }) {
 function Welcome() {
   const navigate = useNavigate();
 
-
-  // TODO: Make mobileLayout be changeable in settings
-  // TODO: Handle resize Events
-  const {width, height} = useWindowDimensions()
-  const [mobileLayout, setModileLayout] = useState(width < 800)
-
   /** Only for mobile layout */
   const [pageNumber, setPageNumber] = useState(0)
 
   const gameId = React.useContext(GameIdContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
+  const {mobile} = React.useContext(MobileContext)
+
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
   const difficulty = useSelector(selectDifficulty(gameId))
@@ -199,7 +196,7 @@ function Welcome() {
     <Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}>
       <CircularProgress />
     </Box>
-    : mobileLayout ?
+    : mobile ?
       (pageNumber == 0 ?
         <div className="column">
           <div className="mobile-nav">