add command line #26

client/src/app.css

@@ -4,7 +4,7 @@
   --clr-primary: #1976d2;
   --clr-code: rgba(0, 32, 90, 0.87);
   --ff-primary: Roboto;
-  --ff-code: Roboto Mono;
+  --ff-code: "Roboto Mono";
 }
 
 

client/src/components/Level.tsx

@@ -100,6 +100,7 @@ const Drawer = styled(MuiDrawer, { shouldForwardProp: (prop) => prop !== 'open'
 /** End Drawer Test */
 
 
+export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(null as any);
 
 function Level() {
 
@@ -194,7 +195,9 @@ function Level() {
 
 
           <EditorContext.Provider value={editorConnection}>
-            {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
+            <MonacoEditorContext.Provider value={editor}>
+              {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
+            </MonacoEditorContext.Provider>
           </EditorContext.Provider>
         </Grid>
       </Grid>

client/src/components/infoview/CommandLine.tsx

@@ -0,0 +1,53 @@
+import * as React from 'react'
+import { useRef, useState } from 'react'
+import { LspDiagnosticsContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
+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'
+
+
+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 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());
+    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) {
+        commandInput.current!.value = "";
+        editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
+      }
+    }
+  }, []);
+
+  return <div className="command-line">
+      <form onSubmit={handleSubmit}>
+        <input type="text" ref={commandInput} disabled={processing} />
+        <input type="submit" value="Run" disabled={processing} />
+      </form>
+    </div>
+}

client/src/components/infoview/goals.tsx

@@ -8,6 +8,7 @@ import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infov
 import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
 import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpcApi';
 import { Hints } from './hints';
+import { CommandLine } from './CommandLine';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -133,7 +134,7 @@ export const Goal = React.memo((props: GoalProps) => {
             undefined,
         [locs, goal.mvarId])
     const goalLi = <div key={'goal'}>
-        <div className="goal-title">Goal: </div>
+        <div className="goal-title">Target: </div>
         <LocationsContext.Provider value={goalLocs}>
             <InteractiveCode fmt={goal.type} />
         </LocationsContext.Provider>
@@ -156,6 +157,7 @@ export const Goal = React.memo((props: GoalProps) => {
         { assumptionHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
+        <CommandLine />
         {!filter.reverse && goalLi}
         {showHints && hints}
     </div>

client/src/components/infoview/infoview.css

@@ -35,3 +35,11 @@
   font-size: 1.8rem;
   font-weight: 500;
 }
+
+.command-line {
+  font-family: var(--ff-primary);
+}
+
+.command-line input[type="text"] {
+  font-family: var(--vscode-editor-font-family);
+}