diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index a538ad2..39c5566 100644
--- 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
{command}
-
}
@@ -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
index 49836ef..e29b914 100644
--- 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 {