undo button

client/src/components/infoview/CommandLine.tsx

@@ -4,43 +4,67 @@ import { LspDiagnosticsContext } from '../../../../node_modules/lean4-infoview/s
 import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol';
-import { MonacoEditorContext } from '../Level'
+import { InputModeContext, MonacoEditorContext } from '../Level'
 
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
 
 
+function hasErrorsOrWarnings(diags) {
+  return diags.some(
+    (d) =>
+      !d.message.startsWith("unsolved goals") &&
+      (d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning)
+  )
+}
+
 export function CommandLine() {
 
   const editor = React.useContext(MonacoEditorContext)
   const commandInput = useRef<HTMLInputElement>()
   const [processing, setProcessing] = useState(false)
 
-  // const allDiags = React.useContext(LspDiagnosticsContext)
-  // const fileDiags = allDiags.get(editor.getModel().uri.toString())
+  const { commandLineMode } = React.useContext(InputModeContext)
+  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()
+      if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
+        editor.executeEdits("command-line", [{
+          range: monaco.Selection.fromPositions(endPos, endPos),
+          text: "\n",
+          forceMoveMarkers: false
+        }]);
+      }
+      editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
+    }
+  }, [commandLineMode])
 
   const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
     ev.preventDefault()
-    var selection = monaco.Selection.fromPositions(
-      editor.getPosition(),
-      editor.getModel().getFullModelRange().getEndPosition()
-    );
-    var text = commandInput.current!.value + "\n";
-    var op = {range: selection, text: text, forceMoveMarkers: false};
-    editor.executeEdits("my-source", [op], editor.getSelections());
+    editor.executeEdits("command-line", [{
+      range: monaco.Selection.fromPositions(
+        editor.getPosition(),
+        editor.getModel().getFullModelRange().getEndPosition()
+      ),
+      text: commandInput.current!.value + "\n",
+      forceMoveMarkers: false
+    }]);
     setProcessing(true)
   }
 
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == editor.getModel().uri.toString()) {
       setProcessing(false)
-      const hasErrorsOrWarnings = params.diagnostics.some(
-        (d) =>
-          !d.message.startsWith("unsolved goals") &&
-          (d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning)
-      )
-      if (!hasErrorsOrWarnings) {
+      if (!hasErrorsOrWarnings(params.diagnostics)) {
         commandInput.current!.value = "";
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
       }
@@ -50,7 +74,7 @@ export function CommandLine() {
   return <div className="command-line">
       <form onSubmit={handleSubmit}>
         <input type="text" ref={commandInput} disabled={processing} />
-        <button type="submit" disabled={processing} className="btn"><FontAwesomeIcon icon={faWandMagicSparkles} /> Run</button>
+        <button type="submit" disabled={processing} className="btn btn-inverted"><FontAwesomeIcon icon={faWandMagicSparkles} /> Run</button>
       </form>
     </div>
 }

client/src/components/infoview/info.tsx

@@ -112,7 +112,6 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
     }), [selectedLocs])
 
     const goalFilter = { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }
-
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
     return <>
         {hasError &&
@@ -121,13 +120,13 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                 <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
             </div>}
         <LocationsContext.Provider value={locs}>
-            {goals && goals.goals.length > 0 && <div className="goals-section">
-                    <div className="goals-section-title">Main Goal</div>
-                    <Goal filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
-                </div>}
+            <div className="goals-section">
+                { goals && goals.goals.length > 0
+                  ? <><div className="goals-section-title">Main Goal</div>
+                    <Goal filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} /></>
+                  : <div className="goals-section-title">No Goals</div> }
+            </div>
         </LocationsContext.Provider>
-        {/* <FilteredGoals headerChildren='Expected type' key='term-goal'
-            goals={termGoal !== undefined ? {goals: [{...termGoal, hints: []}]} : undefined} /> */}
         {userWidgets.map(widget =>
             <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
                 <summary className='mv2 pointer'>{widget.name}</summary>
@@ -135,14 +134,6 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     selectedLocations={selectedLocs} widget={widget}/>
             </details>
         )}
-        {/* <div style={{display: hasMessages ? 'block' : 'none'}} key='messages'>
-            <details key='messages' open>
-                <summary className='mv2 pointer'>Messages ({messages.length})</summary>
-                <div className='ml1'>
-                    <MessagesList uri={pos.uri} messages={messages} />
-                </div>
-            </details>
-        </div> */}
         {nothingToShow && (
             isPaused ?
                 /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */