fix locked editor mode

leanprover-community · Mar 22, 2024 · ce9f5c7 · ce9f5c7
1 parent f428294
commit ce9f5c7
Show file tree

Hide file tree

Showing 6 changed files with 26 additions and 25 deletions.
diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx
@@ -98,23 +98,23 @@ function PreviousButton({setNavOpen}) {
 /** button to toggle between editor and typewriter */
 function InputModeButton({setNavOpen, isDropdown}) {
   const {levelId} = React.useContext(WorldLevelIdContext)
-  const {typewriterMode, setTypewriterMode, lockInputMode} = React.useContext(InputModeContext)
+  const {typewriterMode, setTypewriterMode, lockEditorMode} = React.useContext(InputModeContext)
 
   /** toggle input mode if allowed */
   function toggleInputMode(ev: React.MouseEvent) {
-    if (!lockInputMode){
+    if (!lockEditorMode){
       setTypewriterMode(!typewriterMode)
       setNavOpen(false)
     }
   }
 
   return <Button
-      className={`btn btn-inverted ${isDropdown? '' : 'toggle-width'}`} disabled={levelId <= 0 || lockInputMode}
+      className={`btn btn-inverted ${isDropdown? '' : 'toggle-width'}`} disabled={levelId <= 0 || lockEditorMode}
       inverted="true" to=""
       onClick={(ev) => toggleInputMode(ev)}
-      title={lockInputMode ? "Editor mode is enforced!" : typewriterMode ? "Editor mode" : "Typewriter mode"}>
-    <FontAwesomeIcon icon={typewriterMode ? faCode : faTerminal} />
-    {isDropdown && (typewriterMode ? <>&nbsp;Editor mode</> : <>&nbsp;Typewriter mode</>)}
+      title={lockEditorMode ? "Editor mode is enforced!" : typewriterMode ? "Editor mode" : "Typewriter mode"}>
+    <FontAwesomeIcon icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal} />
+    {isDropdown && ((typewriterMode && !lockEditorMode) ? <>&nbsp;Editor mode</> : <>&nbsp;Typewriter mode</>)}
   </Button>
 }
 

diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts
@@ -125,13 +125,13 @@ export const InputModeContext = React.createContext<{
   setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
   typewriterInput: string,
   setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
-  lockInputMode: boolean,
-  setLockInputMode: React.Dispatch<React.SetStateAction<boolean>>,
+  lockEditorMode: boolean,
+  setLockEditorMode: React.Dispatch<React.SetStateAction<boolean>>,
 }>({
   typewriterMode: true,
   setTypewriterMode: () => {},
   typewriterInput: "",
   setTypewriterInput: () => {},
-  lockInputMode: false,
-  setLockInputMode: () => {},
+  lockEditorMode: false,
+  setLockEditorMode: () => {},
 });
diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
@@ -170,7 +170,6 @@ export const Goal = React.memo((props: GoalProps) => {
     // const hints = <Hints hints={goal.hints} key={goal.mvarId} />
     const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
     const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
-    const {typewriterMode} = React.useContext(InputModeContext)
 
     return <div>
         {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
@@ -181,7 +180,6 @@ export const Goal = React.memo((props: GoalProps) => {
         {!typewriter && 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> }
-        {/* {typewriter && typewriterMode && <Typewriter />} */}
         {!filter.reverse && goalLi}
         {/* {showHints && hints} */}
     </div>

diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
@@ -43,9 +43,9 @@ import { DiagnosticSeverity } from 'vscode-languageclient';
  */
 export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize }) {
   const ec = React.useContext(EditorContext)
-  const { typewriterMode } = React.useContext(InputModeContext)
+  const { typewriterMode, lockEditorMode } = React.useContext(InputModeContext)
   return <>
-    <div className={typewriterMode ? 'hidden' : ''}>
+    <div className={(typewriterMode && !lockEditorMode) ? 'hidden' : ''}>
       <ExerciseStatement data={level} showLeanStatement={true} />
       <div ref={codeviewRef} className={'codeview'}></div>
     </div>
@@ -61,7 +61,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize })
 function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: string, levelId: number, level: LevelInfo, worldSize: number }) {
   const ec = React.useContext(EditorContext)
   const gameId = React.useContext(GameIdContext)
-  const { typewriterMode } = React.useContext(InputModeContext)
+  const { typewriterMode, lockEditorMode } = React.useContext(InputModeContext)
 
   const {proof, setProof} = React.useContext(ProofContext)
 
@@ -111,7 +111,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
         <WithRpcSessions>
           <WithLspDiagnosticsContext>
             <ProgressContext.Provider value={allProgress}>
-              {typewriterMode ?
+              {(typewriterMode && !lockEditorMode) ?
                 <TypewriterInterfaceWrapper world={worldId} level={levelId} data={level} worldSize={worldSize}/>
                 :
                 <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} data={level} />

diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx
@@ -79,7 +79,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         message = diag.message
     }
 
-    const { typewriterMode } = React.useContext(InputModeContext)
+    const { typewriterMode, lockEditorMode } = React.useContext(InputModeContext)
 
     return (
     // <details open>
@@ -98,7 +98,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         //     </span>
         // </summary>
         <div className={severityClass + ' ml1 message'}>
-            {!typewriterMode && <p className="mv2">{title}</p>}
+            {!(typewriterMode && !lockEditorMode) && <p className="mv2">{title}</p>}
             <pre className="font-code pre-wrap">
                 <InteractiveMessage fmt={message} />
             </pre>

diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
@@ -222,7 +222,7 @@ function PlayableLevel({impressum, setImpressum}) {
   const [pageNumber, setPageNumber] = useState(0)
 
   // set to true to prevent switching between typewriter and editor
-  const [lockInputMode, setLockInputMode] = useState(false)
+  const [lockEditorMode, setLockEditorMode] = useState(false)
   const [typewriterInput, setTypewriterInput] = useState("")
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
 
@@ -282,10 +282,11 @@ function PlayableLevel({impressum, setImpressum}) {
   // a hint at the beginning of the proof...
   const [selectedStep, setSelectedStep] = useState<number>()
 
+
   useEffect (() => {
     // Lock editor mode
     if (level?.data?.template) {
-      setTypewriterMode(false)
+      setLockEditorMode(true)
 
       if (editor) {
         let code = editor.getModel().getLinesContent()
@@ -312,6 +313,8 @@ function PlayableLevel({impressum, setImpressum}) {
           console.debug(`not inserting template.`)
         }
       }
+    } else {
+      setLockEditorMode(false)
     }
   }, [level, levelId, worldId, gameId, editor])
 
@@ -326,7 +329,7 @@ function PlayableLevel({impressum, setImpressum}) {
   }, [gameId, worldId, levelId])
 
   useEffect(() => {
-    if (!typewriterMode && editor) {
+    if (!(typewriterMode && !lockEditorMode) && editor) {
       // Delete last input attempt from command line
       editor.executeEdits("typewriter", [{
         range: editor.getSelection(),
@@ -335,7 +338,7 @@ function PlayableLevel({impressum, setImpressum}) {
       }]);
       editor.focus()
     }
-  }, [typewriterMode])
+  }, [typewriterMode, lockEditorMode])
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
@@ -355,7 +358,7 @@ function PlayableLevel({impressum, setImpressum}) {
 
   // Effect when command line mode gets enabled
   useEffect(() => {
-    if (onigasmH && editor && typewriterMode) {
+    if (onigasmH && editor && (typewriterMode && !lockEditorMode)) {
       let code = editor.getModel().getLinesContent().filter(line => line.trim())
       editor.executeEdits("typewriter", [{
         range: editor.getModel().getFullModelRange(),
@@ -378,13 +381,13 @@ function PlayableLevel({impressum, setImpressum}) {
       //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
       // }
     }
-  }, [editor, typewriterMode, onigasmH == null])
+  }, [editor, typewriterMode, lockEditorMode, onigasmH == null])
 
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
       <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
-        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockInputMode, setLockInputMode}}>
+        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode}}>
           <ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
             <EditorContext.Provider value={editorConnection}>
               <MonacoEditorContext.Provider value={editor}>