Improve input and deletion of typewriter #122

leanprover-community · Oct 21, 2023 · 84ad619 · 84ad619
1 parent b6bc778
commit 84ad619
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 3 deletions.
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
@@ -233,8 +233,8 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
   if (!command) { return <></> }
   return <div className="command">
     <div className="command-text">{command}</div>
-    <Button to="" className="undo-button btn btn-inverted" title="Delete this and future commands" onClick={deleteProof}>
-      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Delete
+    <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
+      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
     </Button>
   </div>
 }
@@ -319,6 +319,7 @@ export function TypewriterInterface(props: { world: string, level: number, data:
   const uri = model.uri.toString()
   const gameId = React.useContext(GameIdContext)
   const { proof } = React.useContext(ProofContext)
+  const { setTypewriterInput } = React.useContext(InputModeContext)
   const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
   const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
 
@@ -349,6 +350,7 @@ export function TypewriterInterface(props: { world: string, level: number, data:
         forceMoveMarkers: false
       }])
       setSelectedStep(undefined)
+      setTypewriterInput(proof[line].command)
       ev.stopPropagation()
     }
   }

diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx
@@ -200,6 +200,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
         text: typewriterInput.trim() + "\n",
         forceMoveMarkers: false
       }])
+      setTypewriterInput('')
     }
 
     editor.setPosition(pos)
@@ -211,13 +212,19 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     }
   }, [typewriterInput])
 
+  useEffect(() => {
+    if (proof.length && hasInteractiveErrors(proof[proof.length - 1].errors)) {
+      setTypewriterInput(proof[proof.length - 1].command)
+    }
+  }, [proof])
+
   // React when answer from the server comes back
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == uri) {
       setProcessing(false)
       loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
-        setTypewriterInput("")
+        //setTypewriterInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
       }
     } else {