move command line to bottom

client/src/components/Level.tsx

@@ -9,7 +9,6 @@ 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 {Inventory, Documentation} from './Inventory';
 import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 import 'lean4web/client/src/editor/vscode.css';
@@ -19,31 +18,29 @@ 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 { Button } from './Button'
-import { ConnectionContext, useLeanClient } from '../connection';
-import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api';
-import { changedSelection, codeEdited, selectCode, selectSelections, progressSlice, selectCompleted } from '../state/progress';
-import { useAppDispatch, useAppSelector } from '../hooks';
 import { 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 { EditorInterface, CommandLineInterface } from './infoview/main'
 import type { Location } from 'vscode-languageserver-protocol';
-
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faHome, faArrowRight, faArrowLeft, faRotateLeft } from '@fortawesome/free-solid-svg-icons'
-
 import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles';
-import Markdown from './Markdown';
-
 import Split from 'react-split'
 import { Alert } from '@mui/material';
-import { GameIdContext } from '../App';
 
-import { GameHint } from './infoview/rpcApi';
+import { Button } from './Button'
+import {Inventory, Documentation} from './Inventory';
+import Markdown from './Markdown';
+import { EditorInterface, CommandLineInterface } from './infoview/main'
 import { Hints } from './infoview/hints';
+import { GameHint } from './infoview/rpcApi';
+import { GameIdContext } from '../App';
+import { ConnectionContext, useLeanClient } from '../connection';
+import { useAppDispatch, useAppSelector } from '../hooks';
+import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api';
+import { changedSelection, codeEdited, selectCode, selectSelections, progressSlice, selectCompleted } from '../state/progress';
+
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(null as any);
 
@@ -59,6 +56,7 @@ export const HintContext = React.createContext<{
   setHints: () => {},
 });
 
+
 export const InputModeContext = React.createContext<{
   commandLineMode: boolean,
   setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
@@ -86,17 +84,6 @@ function Level() {
   }
 }
 
-// The mathematical formulation of the statement, supporting e.g. Latex
-// It takes three forms, depending on the precence of name and description:
-// - Theorem xyz: description
-// - Theorem xyz
-// - Exercises: description
-function ExerciseStatement({data}) {
-  return <div className="exercise-statement"><Markdown>
-    {(data?.statementName ? `**Theorem** \`${data?.statementName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}` }
-  </Markdown></div>
-}
-
 function PlayableLevel({worldId, levelId}) {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const chatPanelRef = useRef<HTMLDivElement>(null)
@@ -271,7 +258,6 @@ function PlayableLevel({worldId, levelId}) {
         <div className="exercise-panel">
           <EditorContext.Provider value={editorConnection}>
           <MonacoEditorContext.Provider value={editor}>
-          <ExerciseStatement data={level?.data} />
           <div className="exercise">
             {/* We need the editor to always there and hidden because
               the command line edits its content */}
@@ -280,7 +266,7 @@ function PlayableLevel({worldId, levelId}) {
             { // TODO: Is there any possibility that the editor connection takes a while
               // and we should show a circular progress here?
               commandLineMode && editorConnection &&
-                <CommandLineInterface world={worldId} level={levelId}/>
+                <CommandLineInterface world={worldId} level={levelId} data={level?.data}/>
             }
           </div>
           </MonacoEditorContext.Provider>

client/src/components/infoview/goals.tsx

@@ -170,7 +170,7 @@ export const Goal = React.memo((props: GoalProps) => {
         {!commandLine && assumptionHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {commandLine && commandLineMode && <CommandLine />}
+        {/* {commandLine && commandLineMode && <CommandLine />} */}
         {!filter.reverse && goalLi}
         {/* {showHints && hints} */}
     </div>

client/src/components/infoview/info.tsx

@@ -128,7 +128,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
           <div className="goals-section">
             { goals &&  goals.goals.length > 0 && <>
               <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
-              <ProofDisplay proof={proof}/>
+              {/* <ProofDisplay proof={proof}/> */}
               <OtherGoals filter={goalFilter} goals={goals.goals} />
             </>}
           </div>

client/src/components/infoview/infoview.css

@@ -41,7 +41,7 @@
   padding: 0.5em;
   font-family: var(--ff-primary);
   border-radius: 0.2em;
-  margin: 0.2em 0;
+  margin: 0.2em 0 0;
 }
 
 .command-line form {

client/src/components/infoview/main.tsx

@@ -21,6 +21,20 @@ import { useAppDispatch, useAppSelector } from '../../hooks';
 import { levelCompleted, selectCompleted } from '../../state/progress';
 import { GameIdContext } from '../../App';
 import { InputModeContext } from '../Level';
+import { CommandLine } from './CommandLine';
+import Markdown from '../Markdown';
+import { LevelInfo } from '../../state/api';
+
+// The mathematical formulation of the statement, supporting e.g. Latex
+// It takes three forms, depending on the precence of name and description:
+// - Theorem xyz: description
+// - Theorem xyz
+// - Exercises: description
+function ExerciseStatement({data}) {
+  return <div className="exercise-statement"><Markdown>
+    {(data?.statementName ? `**Theorem** \`${data?.statementName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}` }
+  </Markdown></div>
+}
 
 // TODO: This is only used in `EditorInterface`
 // while `CommandLineInterface` has this copy-pasted in.
@@ -110,6 +124,7 @@ export function EditorInterface({data, codeviewRef, hidden, worldId, levelId, ed
   const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext)
 
   return <div className={hidden ? 'hidden' : ''}>
+    <ExerciseStatement data={data} />
     <div className={`statement ${commandLineMode ? 'hidden' : ''}`}><code>{data?.descrFormat}</code></div>
     <div ref={codeviewRef} className={'codeview'}></div>
     {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
@@ -117,7 +132,7 @@ export function EditorInterface({data, codeviewRef, hidden, worldId, levelId, ed
   </div>
 }
 
-export function CommandLineInterface(props: {world: string, level: number}) {
+export function CommandLineInterface(props: {world: string, level: number, data: LevelInfo}) {
 
   const ec = React.useContext(EditorContext);
   const gameId = React.useContext(GameIdContext)
@@ -177,13 +192,18 @@ export function CommandLineInterface(props: {world: string, level: number}) {
   } else if (serverStoppedResult){
       ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
   } else {
-      ret = <div className="infoview vscode-light">
+      //className="infoview vscode-light"
-          {completed && <div className="level-completed">Level completed! 🎉</div>}
+      ret = <div className="commandline-interface">
-          <Infos />
+          {/* {completed && <div className="level-completed">Level completed! 🎉</div>} */}
+          <div className="content">
+            <ExerciseStatement data={props.data} />
+            <Infos />
+          </div>
+          <CommandLine />
       </div>
   }
 
-  return <div>
+  return <>
     {/* <button className="btn" onClick={handleUndo} disabled={!canUndo}><FontAwesomeIcon icon={faRotateLeft} /> Undo</button> */}
     <ConfigContext.Provider value={config}>
       <VersionContext.Provider value={serverVersion}>
@@ -196,7 +216,7 @@ export function CommandLineInterface(props: {world: string, level: number}) {
         </WithRpcSessions>
       </VersionContext.Provider>
     </ConfigContext.Provider>
-  </div>
+  </>
 
 
 }

client/src/components/level.css

@@ -29,11 +29,14 @@
   overflow: auto;
 }
 
-.chat-panel, .infoview, .exercise, .exercise-statement {
+.chat-panel, .infoview, .exercise {
   padding-top: 1em;
+  padding-bottom: 0;
+}
+
+.chat-panel, .infoview, .exercise-statement {
   padding-left: 1em;
   padding-right: 1em;
-  padding-bottom: 0;
 }
 
 .conclusion {
@@ -172,6 +175,10 @@ td code  {
   margin: 1px;
 } */
 
+.exercise {
+  height: 100%;
+}
+
 .chat {
   height: calc(100% - 3.5em);
   overflow-y: scroll;
@@ -182,3 +189,24 @@ td code  {
   height: 3.5em;
   border-top:  0.1em solid #aaa;
 }
+
+/* .exercise-panel {
+  display: flex;
+  flex-flow: column;
+  height: 100%;
+} */
+
+.commandline-interface {
+  display: flex;
+  flex-flow: column;
+  height: 100%;
+}
+
+.command-line {
+  flex: 0 1 auto;
+}
+
+.commandline-interface .content {
+  flex: 1 1 auto;
+  overflow-y: scroll;
+}