monaco command line

client/src/components/infoview/CommandLine.tsx

@@ -1,5 +1,5 @@
 import * as React from 'react'
-import { useRef, useState } from 'react'
+import { useRef, useState, useEffect } 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'
@@ -28,7 +28,51 @@ export function CommandLine() {
   const allDiags = React.useContext(LspDiagnosticsContext)
   const diags = allDiags.get(editor.getModel().uri.toString())
 
-  React.useEffect(() => {
+  const inputRef = useRef()
+
+  useEffect(() => {
+    const editor = monaco.editor.create(inputRef.current!, {
+      quickSuggestions: false,
+      lightbulb: {
+        enabled: true
+      },
+      unicodeHighlight: {
+          ambiguousCharacters: false,
+      },
+      automaticLayout: true,
+      minimap: {
+        enabled: false
+      },
+      lineNumbers: 'off',
+      glyphMargin: false,
+      folding: false,
+      // Undocumented see https://github.com/Microsoft/vscode/issues/30795#issuecomment-410998882
+      lineDecorationsWidth: 0,
+      lineNumbersMinChars: 0,
+      'semanticHighlighting.enabled': true,
+      overviewRulerLanes: 0,
+      hideCursorInOverviewRuler: true,
+      scrollbar: {
+          vertical: 'hidden'
+      },
+      overviewRulerBorder: false,
+      theme: 'vs-code-theme-converted',
+      contextmenu: false
+    })
+
+    const t = editor.getModel().onDidChangeContent((e) => {
+      const value = editor.getValue()
+      const newValue = value.replace(/[\n\r]/g, '')
+      if (value != newValue) {
+        editor.setValue(newValue)
+      }
+    })
+
+    return () => {t.dispose(); editor.dispose()}
+  }, [])
+
+  // Effect when command line mode gets enabled
+  useEffect(() => {
     if (commandLineMode) {
       const endPos = editor.getModel().getFullModelRange().getEndPosition()
       if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
@@ -42,6 +86,7 @@ export function CommandLine() {
     }
   }, [commandLineMode])
 
+  // Run the command
   const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
     ev.preventDefault()
     const pos = editor.getPosition()
@@ -57,6 +102,7 @@ export function CommandLine() {
     setProcessing(true)
   }
 
+  // React when answer from the server comes back
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == editor.getModel().uri.toString()) {
       setProcessing(false)
@@ -69,7 +115,8 @@ export function CommandLine() {
 
   return <div className="command-line">
       <form onSubmit={handleSubmit}>
-        <input type="text" ref={commandInput} disabled={processing} />
+        <div ref={inputRef} className="command-line-input" />
+        {/* <input type="text" ref={commandInput} disabled={processing} /> */}
         <button type="submit" disabled={processing} className="btn btn-inverted"><FontAwesomeIcon icon={faWandMagicSparkles} /> Run</button>
       </form>
     </div>

client/src/components/infoview/infoview.css

@@ -44,10 +44,6 @@
   margin: 0.2em 0;
 }
 
-.command-line input[type="text"] {
-  font-family: var(--vscode-editor-font-family);
-}
-
 .command-line form {
   display: flex;
 }
@@ -56,7 +52,7 @@
   display: block;
 }
 
-.command-line form>input[type="text"]{
+.command-line .command-line-input{
   flex: 1;
   padding: 0.2em .6em;
   font-size: 1rem;