From 48de58416dbe1207b3c2acdb55fdafcab1ec949c Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 30 Jan 2023 12:00:33 +0100
Subject: [PATCH] editor mode

---
 client/src/components/Level.tsx          | 19 +++++++++++++++----
 client/src/components/infoview/goals.tsx |  6 +++++-
 client/src/components/level.css          |  4 ++++
 3 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 575841c..604b2cc 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -45,6 +45,11 @@ import Split from 'react-split'
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(null as any);
 
+export const InputModeContext = React.createContext<{
+  commandLineMode: boolean,
+  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>
+}>({commandLineMode: true, setCommandLineMode: () => {}});
+
 function Level() {
 
   const params = useParams();
@@ -54,6 +59,7 @@ function Level() {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const introductionPanelRef = useRef<HTMLDivElement>(null)
 
+  const [commandLineMode, setCommandLineMode] = useState(true)
   const [showSidePanel, setShowSidePanel] = useState(true)
 
   const toggleSidePanel = () => {
@@ -106,7 +112,7 @@ function Level() {
       </div>
 
     </div>
-    <Split minSize={200} className={`app-content level ${level.isLoading ? 'hidden' : ''}}`}>
+    <Split minSize={200} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
       <div className="main-panel">
         <div ref={introductionPanelRef} className="introduction-panel">
           <Markdown>{level?.data?.introduction}</Markdown>
@@ -114,14 +120,19 @@ function Level() {
         <div className="exercise">
           <h4>Aufgabe:</h4>
           <Markdown>{level?.data?.descrText}</Markdown>
-          <div className="statement"><code>{level?.data?.descrFormat}</code></div>
-          <div ref={codeviewRef} className="codeview"></div>
+          <div className={`statement ${commandLineMode ? 'hidden' : ''}`}><code>{level?.data?.descrFormat}</code></div>
+          <div ref={codeviewRef} className={`codeview ${commandLineMode ? 'hidden' : ''}`}></div>
         </div>
       </div>
       <div className="info-panel">
+        <FormGroup className="input-mode-switch">
+          <FormControlLabel control={<Switch onChange={(ev) => { setCommandLineMode(!commandLineMode) }} />} label="Editor mode" />
+        </FormGroup>
         <EditorContext.Provider value={editorConnection}>
           <MonacoEditorContext.Provider value={editor}>
-            {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
+            <InputModeContext.Provider value={{commandLineMode, setCommandLineMode}}>
+              {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
+            </InputModeContext.Provider>
           </MonacoEditorContext.Provider>
         </EditorContext.Provider>
       </div>
diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
index 6b7f198..bf64057 100644
--- a/client/src/components/infoview/goals.tsx
+++ b/client/src/components/infoview/goals.tsx
@@ -9,6 +9,7 @@ import { Locations, LocationsContext, SelectableLocation } from '../../../../nod
 import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpcApi';
 import { Hints } from './hints';
 import { CommandLine } from './CommandLine';
+import { InputModeContext } from '../Level';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -147,6 +148,7 @@ export const Goal = React.memo((props: GoalProps) => {
     const hints = <Hints hints={goal.hints} />
     const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
     const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
+    const {commandLineMode} = React.useContext(InputModeContext)
 
     return <div className={cn}>
         {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
@@ -157,7 +159,9 @@ export const Goal = React.memo((props: GoalProps) => {
         { 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 />
+        <div className={commandLineMode ? "" : "hidden"}>
+            <CommandLine />
+        </div>
         {!filter.reverse && goalLi}
         {showHints && hints}
     </div>
diff --git a/client/src/components/level.css b/client/src/components/level.css
index b094a8f..e6bab61 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -59,6 +59,10 @@
   margin-bottom: 0;
 }
 
+.input-mode-switch {
+  float: right;
+}
+
 .doc-panel li {
   border-bottom: 1px solid rgba(0, 0, 0, 0.12); /* This should be teh same colour as `divider` in LeftPanel.tsx */
 }