repair command line

client/src/components/infoview/CommandLine.tsx

@@ -170,21 +170,6 @@ export function CommandLine() {
     return () => { l.dispose() }
   }, [oneLineEditor, runCommand])
 
-  // Effect when command line mode gets enabled
-  useEffect(() => {
-    if (commandLineMode) {
-      const endPos = editor.getModel().getFullModelRange().getEndPosition()
-      if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
-        editor.executeEdits("command-line", [{
-          range: monaco.Selection.fromPositions(endPos, endPos),
-          text: commandLineInput + "\n",
-          forceMoveMarkers: false
-        }]);
-      }
-      editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
-    }
-  }, [commandLineMode])
-
   const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
     ev.preventDefault()
     runCommand()

client/src/components/infoview/main.tsx

@@ -18,7 +18,7 @@ import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '.
 import { WithRpcSessions } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infoview/serverVersion';
 import { useAppDispatch, useAppSelector } from '../../hooks';
-import { codeEdited, levelCompleted, selectCompleted } from '../../state/progress';
+import { levelCompleted, selectCompleted } from '../../state/progress';
 
 
 export function Main(props: {world: string, level: number}) {