diff --git a/client/src/components/infoview/CommandLine.tsx b/client/src/components/infoview/CommandLine.tsx index 06960e4..d86c908 100644 --- a/client/src/components/infoview/CommandLine.tsx +++ b/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 = (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
- +
+ {/* */}
diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css index c3d4145..174d4f1 100644 --- a/client/src/components/infoview/infoview.css +++ b/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;