From 7b26280ae92ddcb62c5b48b66a6f13607c089c7e Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sat, 7 Oct 2023 22:07:02 +0200
Subject: [PATCH] rename commandline to typewriter #107

---
 client/src/components/app_bar.tsx             | 17 +++++-----
 .../src/components/infoview/command_line.tsx  | 32 +++++++++----------
 client/src/components/infoview/context.ts     | 16 +++++-----
 client/src/components/infoview/goals.tsx      | 16 +++++-----
 client/src/components/infoview/info.tsx       |  4 +--
 client/src/components/infoview/infoview.css   | 18 +++++------
 client/src/components/infoview/main.tsx       | 32 +++++++++----------
 client/src/components/infoview/messages.tsx   | 12 +++----
 client/src/components/level.css               | 10 +++---
 client/src/components/level.tsx               | 24 +++++++-------
 10 files changed, 91 insertions(+), 90 deletions(-)

diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx
index 781489e..6b723d2 100644
--- a/client/src/components/app_bar.tsx
+++ b/client/src/components/app_bar.tsx
@@ -123,7 +123,7 @@ export function WelcomeAppBar({gameInfo, toggleImpressum, openEraseMenu, openUpl
           <FontAwesomeIcon icon={faHome} />&nbsp;Home
         </Button>
         <Button disabled={levelId <= 0} inverted="true" to=""
-            onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
+            onClick={(ev) => { setTypewriterMode(!typewriterMode); setNavOpen(false) }}
             title="toggle Editor mode">
           <FontAwesomeIcon icon={faCode} />&nbsp;Toggle Editor
         </Button> */}
@@ -291,7 +291,7 @@ export function LevelAppBar({
   const difficulty = useSelector(selectDifficulty(gameId))
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
 
-  const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext)
+  const { typewriterMode, setTypewriterMode } = React.useContext(InputModeContext)
 
   const [navOpen, setNavOpen] = React.useState(false)
 
@@ -341,9 +341,10 @@ export function LevelAppBar({
             <FontAwesomeIcon icon={faHome} />&nbsp;Home
           </Button>
           <Button disabled={levelId <= 0} inverted="true" to=""
-              onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
-              title="toggle Editor mode">
-            <FontAwesomeIcon icon={faCode} />&nbsp;Toggle Editor
+              onClick={(ev) => { setTypewriterMode(!typewriterMode); setNavOpen(false) }}
+              title={typewriterMode ? "Editor mode" : "Typewriter mode"}>
+            <FontAwesomeIcon icon={typewriterMode ? faCode : faTerminal} />
+            &nbsp;{typewriterMode ? "Editor mode" : "Typewriter mode"}
           </Button>
           <Button title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
             <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Info &amp; Impressum
@@ -388,9 +389,9 @@ export function LevelAppBar({
             </Button>
           }
           <Button className="btn btn-inverted toggle-width" disabled={levelId <= 0} inverted="true" to=""
-              onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
-              title="toggle Editor mode">
-            <FontAwesomeIcon icon={commandLineMode ? faCode : faTerminal} />
+              onClick={(ev) => { setTypewriterMode(!typewriterMode); setNavOpen(false) }}
+              title={typewriterMode ? "Editor mode" : "Typewriter mode"}>
+            <FontAwesomeIcon icon={typewriterMode ? faCode : faTerminal} />
           </Button>
           <Button className="btn btn-inverted toggle-width" title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
             <FontAwesomeIcon icon={impressum ? faXmark : faCircleInfo} />
diff --git a/client/src/components/infoview/command_line.tsx b/client/src/components/infoview/command_line.tsx
index 8b9f273..145f2df 100644
--- a/client/src/components/infoview/command_line.tsx
+++ b/client/src/components/infoview/command_line.tsx
@@ -64,7 +64,7 @@ config.autoClosingPairs = config.autoClosingPairs.map(
 monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 /** The input field */
-export function CommandLine({hidden}: {hidden?: boolean}) {
+export function Typewriter({hidden}: {hidden?: boolean}) {
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
@@ -74,7 +74,7 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
   const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
 
-  const {commandLineInput, setCommandLineInput} = React.useContext(InputModeContext)
+  const {typewriterInput, setTypewriterInput} = React.useContext(InputModeContext)
 
   const inputRef = useRef()
 
@@ -190,26 +190,26 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
     setDeletedChat([])
 
     const pos = editor.getPosition()
-    if (commandLineInput) {
+    if (typewriterInput) {
       setProcessing(true)
-      editor.executeEdits("command-line", [{
+      editor.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
           pos,
           editor.getModel().getFullModelRange().getEndPosition()
         ),
-        text: commandLineInput.trim() + "\n",
+        text: typewriterInput.trim() + "\n",
         forceMoveMarkers: false
       }])
     }
 
     editor.setPosition(pos)
-  }, [commandLineInput, editor])
+  }, [typewriterInput, editor])
 
   useEffect(() => {
-    if (oneLineEditor && oneLineEditor.getValue() !== commandLineInput) {
-      oneLineEditor.setValue(commandLineInput)
+    if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
+      oneLineEditor.setValue(typewriterInput)
     }
-  }, [commandLineInput])
+  }, [typewriterInput])
 
   // React when answer from the server comes back
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
@@ -217,7 +217,7 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
       setProcessing(false)
       loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
-        setCommandLineInput("")
+        setTypewriterInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
       }
     } else {
@@ -231,7 +231,7 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
 
   useEffect(() => {
     const myEditor = monaco.editor.create(inputRef.current!, {
-      value: commandLineInput,
+      value: typewriterInput,
       language: "lean4cmd",
       quickSuggestions: false,
       lightbulb: {
@@ -274,14 +274,14 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
     // Ensure that our one-line editor can only have a single line
     const l = oneLineEditor.getModel().onDidChangeContent((e) => {
       const value = oneLineEditor.getValue()
-      setCommandLineInput(value)
+      setTypewriterInput(value)
       const newValue = value.replace(/[\n\r]/g, '')
       if (value != newValue) {
         oneLineEditor.setValue(newValue)
       }
     })
     return () => { l.dispose() }
-  }, [oneLineEditor, setCommandLineInput])
+  }, [oneLineEditor, setTypewriterInput])
 
   useEffect(() => {
     if (!oneLineEditor) return
@@ -308,10 +308,10 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
     runCommand()
   }
 
-  return <div className={`command-line${hidden ? ' hidden' : ''}`}>
+  return <div className={`typewriter${hidden ? ' hidden' : ''}`}>
       <form onSubmit={handleSubmit}>
-        <div className="command-line-input-wrapper">
-          <div ref={inputRef} className="command-line-input" />
+        <div className="typewriter-input-wrapper">
+          <div ref={inputRef} className="typewriter-input" />
         </div>
         <button type="submit" disabled={processing} className="btn btn-inverted">
           <FontAwesomeIcon icon={faWandMagicSparkles} /> Execute
diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts
index 27fe0bb..e5b4037 100644
--- a/client/src/components/infoview/context.ts
+++ b/client/src/components/infoview/context.ts
@@ -105,13 +105,13 @@ export const DeletedChatContext = React.createContext<{
 })
 
 export const InputModeContext = React.createContext<{
-  commandLineMode: boolean,
-  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
-  commandLineInput: string,
-  setCommandLineInput: React.Dispatch<React.SetStateAction<string>>
+  typewriterMode: boolean,
+  setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
+  typewriterInput: string,
+  setTypewriterInput: React.Dispatch<React.SetStateAction<string>>
 }>({
-  commandLineMode: true,
-  setCommandLineMode: () => {},
-  commandLineInput: "",
-  setCommandLineInput: () => {},
+  typewriterMode: true,
+  setTypewriterMode: () => {},
+  typewriterInput: "",
+  setTypewriterInput: () => {},
 });
diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
index 08a0d36..6e7049b 100644
--- a/client/src/components/infoview/goals.tsx
+++ b/client/src/components/infoview/goals.tsx
@@ -124,7 +124,7 @@ interface GoalProps {
     goal: InteractiveGoal
     filter: GoalFilterState
     showHints?: boolean
-    commandLine: boolean
+    typewriter: boolean
 }
 
 interface ProofDisplayProps {
@@ -136,7 +136,7 @@ interface ProofDisplayProps {
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
 export const Goal = React.memo((props: GoalProps) => {
-    const { goal, filter, showHints, commandLine } = props
+    const { goal, filter, showHints, typewriter } = props
 
     // TODO: Apparently `goal` can be `undefined`
     if (!goal) {return <></>}
@@ -163,18 +163,18 @@ 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 {commandLineMode} = React.useContext(InputModeContext)
+    const {typewriterMode} = React.useContext(InputModeContext)
 
     return <div>
         {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
         {filter.reverse && goalLi}
-        {! commandLine && objectHyps.length > 0 &&
+        {! typewriter && objectHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Objects:</div>
             {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {!commandLine && assumptionHyps.length > 0 &&
+        {!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> }
-        {/* {commandLine && commandLineMode && <CommandLine />} */}
+        {/* {typewriter && typewriterMode && <Typewriter />} */}
         {!filter.reverse && goalLi}
         {/* {showHints && hints} */}
     </div>
@@ -229,7 +229,7 @@ export const OtherGoals = React.memo((props: GoalProps2) => {
             <summary>
               <InteractiveCode fmt={goal.type} />
             </summary>
-            <Goal commandLine={false} filter={filter} goal={goal} />
+            <Goal typewriter={false} filter={filter} goal={goal} />
           </details>)}
       </div>}
   </>
@@ -264,7 +264,7 @@ export function Goals({ goals, filter }: GoalsProps) {
         return <>No goals</>
     } else {
         return <>
-          {goals.goals.map((g, i) => <Goal commandLine={false} key={i} goal={g} filter={filter} />)}
+          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g} filter={filter} />)}
         </>
     }
 }
diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx
index 1b15983..27f4644 100644
--- a/client/src/components/infoview/info.tsx
+++ b/client/src/components/infoview/info.tsx
@@ -129,7 +129,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
           </div>
           <div>
             { goals && (goals.goals.length > 0
-              ? <Goal commandLine={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
+              ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
               : <div className="goals-section-title">No Goals</div>
             )}
           </div>
@@ -156,7 +156,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     <div className="goals-section-title">Weitere Goals</div>
 
                     {goals.goals.slice(1).map((goal, i) =>
-                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal commandLine={false} filter={goalFilter} goal={goal} /></details>)}
+                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal typewriter={false} filter={goalFilter} goal={goal} /></details>)}
                 </div>}
         </LocationsContext.Provider> */}
     </>
diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css
index d08af8a..4142917 100644
--- a/client/src/components/infoview/infoview.css
+++ b/client/src/components/infoview/infoview.css
@@ -43,7 +43,7 @@
   font-weight: 500;
 }
 
-.command-line {
+.typewriter {
   background: var(--clr-primary);
   padding: 0.5em;
   font-family: var(--ff-primary);
@@ -51,17 +51,17 @@
   /* margin: 0.2em 0 0; */
 }
 
-.command-line form {
+.typewriter form {
   display: flex;
 }
 
-.command-line button, .undo-button {
+.typewriter button, .undo-button {
   display: block;
   white-space: nowrap;
   flex: 0;
 }
 
-.command-line .command-line-input-wrapper{
+.typewriter .typewriter-input-wrapper{
   min-width: 0;
   flex: 1;
   padding: 0.4em .6em 0;
@@ -71,15 +71,15 @@
   flex-direction: column;
 }
 
-.command-line .command-line-input {
+.typewriter .typewriter-input {
   flex: 1;
 }
 
 /* Turn off some monaco decorations: */
-.command-line-input .monaco-editor .view-overlays .current-line {
+.typewriter-input .monaco-editor .view-overlays .current-line {
   border: 0;
 }
-.command-line-input .monaco-editor .scroll-decoration {
+.typewriter-input .monaco-editor .scroll-decoration {
   box-shadow: none;
 }
 
@@ -138,7 +138,7 @@
 
 
 /* Push the goals to the bottom for now, until we insert the proof history above. */
-.commandline-interface .content {
+.typewriter-interface .content {
   display: flex;
   flex-direction: column;
   scroll-behavior: smooth;
@@ -149,7 +149,7 @@
   scroll-behavior: smooth;
 }
 
-.commandline-interface .content .tmp-pusher {
+.typewriter-interface .content .tmp-pusher {
   flex: 1;
 }
 
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index 19afd53..37e2fc4 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -28,7 +28,7 @@ import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
 import { Goal } from './goals';
 import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './context';
-import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line';
+import { Typewriter, hasErrors, hasInteractiveErrors } from './command_line';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
@@ -41,9 +41,9 @@ import { Hints } from '../hints';
  */
 export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize }) {
   const ec = React.useContext(EditorContext)
-  const { commandLineMode } = React.useContext(InputModeContext)
+  const { typewriterMode } = React.useContext(InputModeContext)
   return <>
-    <div className={commandLineMode ? 'hidden' : ''}>
+    <div className={typewriterMode ? 'hidden' : ''}>
       <ExerciseStatement data={level} />
       <div ref={codeviewRef} className={'codeview'}></div>
     </div>
@@ -62,7 +62,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 { commandLineMode } = React.useContext(InputModeContext)
+  const { typewriterMode } = React.useContext(InputModeContext)
 
   // Mark level as completed when server gives notification
   const dispatch = useAppDispatch()
@@ -108,8 +108,8 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
         <WithRpcSessions>
           <WithLspDiagnosticsContext>
             <ProgressContext.Provider value={allProgress}>
-              {commandLineMode ?
-                <CommandLineInterface world={worldId} level={levelId} data={level} worldSize={worldSize}/>
+              {typewriterMode ?
+                <TypewriterInterface world={worldId} level={levelId} data={level} worldSize={worldSize}/>
                 :
                 <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />
               }
@@ -135,7 +135,7 @@ function ExerciseStatement({ data }) {
 }
 
 // TODO: This is only used in `EditorInterface`
-// while `CommandLineInterface` has this copy-pasted in.
+// while `TypewriterInterface` has this copy-pasted in.
 export function Main(props: { world: string, level: number }) {
   const ec = React.useContext(EditorContext);
   const gameId = React.useContext(GameIdContext)
@@ -232,7 +232,7 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 //       message = diag.message
 //   }
 
-//   const { commandLineMode } = React.useContext(InputModeContext)
+//   const { typewriterMode } = React.useContext(InputModeContext)
 
 //   return (
 //   // <details open>
@@ -251,7 +251,7 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 //       //     </span>
 //       // </summary>
 //       <div className={severityClass + ' ml1 message'}>
-//           {!commandLineMode && <p className="mv2">{title}</p>}
+//           {!typewriterMode && <p className="mv2">{title}</p>}
 //           <pre className="font-code pre-wrap">
 //               <InteractiveMessage fmt={message} />
 //           </pre>
@@ -276,13 +276,13 @@ function GoalsTab({ proofStep, last}: { proofStep: ProofStep, last : boolean })
       ))}
     </div>
     <div className="goal-tab vscode-light">
-      <Goal commandLine={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
+      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
     </div>
   </div>
 }
 
 /** The interface in command line mode */
-export function CommandLineInterface(props: { world: string, level: number, data: LevelInfo, worldSize: number }) {
+export function TypewriterInterface(props: { world: string, level: number, data: LevelInfo, worldSize: number }) {
 
   const ec = React.useContext(EditorContext)
   const editor = React.useContext(MonacoEditorContext)
@@ -309,7 +309,7 @@ export function CommandLineInterface(props: { world: string, level: number, data
       })
       setDeletedChat(deletedChat)
 
-      editor.executeEdits("command-line", [{
+      editor.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
           { lineNumber: line, column: 1 },
           editor.getModel().getFullModelRange().getEndPosition()
@@ -420,7 +420,7 @@ export function CommandLineInterface(props: { world: string, level: number, data
   // TODO: does the position matter at all?
   const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
 
-  return <div className="commandline-interface">
+  return <div className="typewriter-interface">
     <RpcContext.Provider value={rpcSess}>
     <div className="content">
       <div className="tmp-pusher">
@@ -438,12 +438,12 @@ export function CommandLineInterface(props: { world: string, level: number, data
                 // entered command as it is still present in the command line.
                 // TODO: Should not use index as key.
                 return <div key={`proof-step-${i}`}>
-                  <Errors errors={step.errors} commandLineMode={true} />
+                  <Errors errors={step.errors} typewriterMode={true} />
                 </div>
               } else {
                 return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')} onClick={toggleSelectStep(i)}>
                   <Command command={step.command} deleteProof={deleteProof(i)} />
-                  <Errors errors={step.errors} commandLineMode={true} />
+                  <Errors errors={step.errors} typewriterMode={true} />
                   {mobile && i == 0 && props.data?.introduction &&
                     <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
                       <Markdown>{props.data?.introduction}</Markdown>
@@ -493,7 +493,7 @@ export function CommandLineInterface(props: { world: string, level: number, data
         }
       </div>
     </div>
-    <CommandLine hidden={!withErr && proof[proof.length - 1]?.goals.length == 0}/>
+    <Typewriter hidden={!withErr && proof[proof.length - 1]?.goals.length == 0}/>
     </RpcContext.Provider>
   </div>
 }
diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx
index fa88f33..700343e 100644
--- a/client/src/components/infoview/messages.tsx
+++ b/client/src/components/infoview/messages.tsx
@@ -18,7 +18,7 @@ interface MessageViewProps {
 }
 
 /** A list of messages (info/warning/error) that are produced after this command */
-function Error({error, commandLineMode} : {error : InteractiveDiagnostic, commandLineMode : boolean}) {
+function Error({error, typewriterMode} : {error : InteractiveDiagnostic, typewriterMode : boolean}) {
   // The first step will always have an empty command
 
   const severityClass = error.severity ? {
@@ -41,7 +41,7 @@ function Error({error, commandLineMode} : {error : InteractiveDiagnostic, comman
   }
 
   return <div className={severityClass + ' ml1 message'}>
-    {!commandLineMode && <p className="mv2">{title}</p>}
+    {!typewriterMode && <p className="mv2">{title}</p>}
     <pre className="font-code pre-wrap">
       <InteractiveMessage fmt={message} />
     </pre>
@@ -50,9 +50,9 @@ function Error({error, commandLineMode} : {error : InteractiveDiagnostic, comman
 
 // TODO: Should not use index as key.
 /** A list of messages (info/warning/error) that are produced after this command */
-export function Errors ({errors, commandLineMode} : {errors : InteractiveDiagnostic[], commandLineMode : boolean}) {
+export function Errors ({errors, typewriterMode} : {errors : InteractiveDiagnostic[], typewriterMode : boolean}) {
   return <div>
-    {errors.map((err, i) => (<Error key={`error-${i}`} error={err} commandLineMode={commandLineMode}/>))}
+    {errors.map((err, i) => (<Error key={`error-${i}`} error={err} typewriterMode={typewriterMode}/>))}
   </div>
 }
 
@@ -79,7 +79,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         message = diag.message
     }
 
-    const { commandLineMode } = React.useContext(InputModeContext)
+    const { typewriterMode } = React.useContext(InputModeContext)
 
     return (
     // <details open>
@@ -98,7 +98,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         //     </span>
         // </summary>
         <div className={severityClass + ' ml1 message'}>
-            {!commandLineMode && <p className="mv2">{title}</p>}
+            {!typewriterMode && <p className="mv2">{title}</p>}
             <pre className="font-code pre-wrap">
                 <InteractiveMessage fmt={message} />
             </pre>
diff --git a/client/src/components/level.css b/client/src/components/level.css
index fd6579f..4439bd9 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -218,17 +218,17 @@ td code  {
   height: 100%;
 } */
 
-.commandline-interface {
+.typewriter-interface {
   display: flex;
   flex-flow: column;
   height: 100%;
 }
 
-.command-line {
+.typewriter {
   flex: 0 1 auto;
 }
 
-.commandline-interface .content {
+.typewriter-interface .content {
   flex: 1 1 auto;
   overflow-y: scroll;
   padding: 0;
@@ -318,11 +318,11 @@ td code  {
   justify-content: center;
 }
 
-.commandline-interface .content, .world-image-container.empty {
+.typewriter-interface .content, .world-image-container.empty {
   background-color: #eee;
 }
 
-.commandline-interface .proof {
+.typewriter-interface .proof {
   background-color: #fff;
 }
 
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 97cf73d..00e3f87 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -212,8 +212,8 @@ function PlayableLevel() {
   const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
   // Only for mobile layout
   const [pageNumber, setPageNumber] = useState(0)
-  const [commandLineMode, setCommandLineMode] = useState(true)
-  const [commandLineInput, setCommandLineInput] = useState("")
+  const [typewriterMode, setTypewriterMode] = useState(true)
+  const [typewriterInput, setTypewriterInput] = useState("")
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
   const dispatch = useAppDispatch()
 
@@ -246,7 +246,7 @@ function PlayableLevel() {
     useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection)
 
   /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
-   * `CommandLineInterface`.
+   * `TypewriterInterface`.
    */
   const handleUndo = () => {
     const endPos = editor.getModel().getFullModelRange().getEndPosition()
@@ -284,23 +284,23 @@ function PlayableLevel() {
   useEffect(() => {
     // TODO: That's a problem if the saved proof contains an error
     // Reset command line input when loading a new level
-    setCommandLineInput("")
+    setTypewriterInput("")
 
     // Load the selected help steps from the store
     setShowHelp(new Set(selectHelp(gameId, worldId, levelId)(store.getState())))
   }, [gameId, worldId, levelId])
 
   useEffect(() => {
-    if (!commandLineMode) {
+    if (!typewriterMode) {
       // Delete last input attempt from command line
-      editor.executeEdits("command-line", [{
+      editor.executeEdits("typewriter", [{
         range: editor.getSelection(),
         text: "",
         forceMoveMarkers: false
       }]);
       editor.focus()
     }
-  }, [commandLineMode])
+  }, [typewriterMode])
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
@@ -320,10 +320,10 @@ function PlayableLevel() {
 
   // Effect when command line mode gets enabled
   useEffect(() => {
-    if (editor && commandLineMode) {
+    if (editor && typewriterMode) {
       let endPos = editor.getModel().getFullModelRange().getEndPosition()
       if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
-        editor.executeEdits("command-line", [{
+        editor.executeEdits("typewriter", [{
           range: monaco.Selection.fromPositions(endPos, endPos),
           text: "\n",
           forceMoveMarkers: true
@@ -332,17 +332,17 @@ function PlayableLevel() {
       endPos = editor.getModel().getFullModelRange().getEndPosition()
       let currPos = editor.getPosition()
       if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
-        // This is not a position that would naturally occur from CommandLine, reset:
+        // This is not a position that would naturally occur from Typewriter, reset:
         editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
       }
     }
-  }, [editor, commandLineMode])
+  }, [editor, typewriterMode])
 
   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={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
+        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput}}>
           <ProofContext.Provider value={{proof, setProof}}>
             <EditorContext.Provider value={editorConnection}>
               <MonacoEditorContext.Provider value={editor}>