Merge branch 'main' of github.com:leanprover-community/lean4game

client/src/components/infoview/CommandLine.tsx

@@ -28,12 +28,6 @@ export function CommandLine() {
   const allDiags = React.useContext(LspDiagnosticsContext)
   const diags = allDiags.get(editor.getModel().uri.toString())
 
-  React.useEffect(() => {
-    if (hasErrorsOrWarnings(diags)) {
-      // alert("err")
-    }
-  }, [])
-
   React.useEffect(() => {
     if (commandLineMode) {
       const endPos = editor.getModel().getFullModelRange().getEndPosition()
@@ -50,14 +44,16 @@ export function CommandLine() {
 
   const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
     ev.preventDefault()
+    const pos = editor.getPosition()
     editor.executeEdits("command-line", [{
       range: monaco.Selection.fromPositions(
-        editor.getPosition(),
+        pos,
         editor.getModel().getFullModelRange().getEndPosition()
       ),
       text: commandInput.current!.value + "\n",
       forceMoveMarkers: false
     }]);
+    editor.setPosition(pos)
     setProcessing(true)
   }