phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

more monaco command line

Browse Source 
fixes #32
This commit is contained in:
Alexander Bentkamp
2023-02-07 15:39:40 +01:00
parent a3b1011035
commit 278aedb20c
4 changed files with 183 additions and 52 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/Level.tsx
+14 -5
View File
@@ -44,8 +44,15 @@ export const MonacoEditorContext = React.createContext<monaco.editor.IStandalone
export const InputModeContext = React.createContext<{
commandLineMode: boolean,
setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>
}>({commandLineMode: true, setCommandLineMode: () => {}});
setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
commandLineInput: string,
setCommandLineInput: React.Dispatch<React.SetStateAction<string>>
}>({
commandLineMode: true,
setCommandLineMode: () => {},
commandLineInput: "",
setCommandLineInput: () => {},
});
function Level() {
@@ -56,9 +63,12 @@ function Level() {
const codeviewRef = useRef<HTMLDivElement>(null)
const introductionPanelRef = useRef<HTMLDivElement>(null)
const initialCode = useSelector(selectCode(worldId, levelId))
const [commandLineMode, setCommandLineMode] = useState(true)
const [commandLineInput, setCommandLineInput] = useState("")
const [showSidePanel, setShowSidePanel] = useState(true)
const [canUndo, setCanUndo] = useState(true)
const [canUndo, setCanUndo] = useState(initialCode.trim() !== "")
const toggleSidePanel = () => {
setShowSidePanel(!showSidePanel)
@@ -119,7 +129,6 @@ function Level() {
setCanUndo(code.trim() !== "")
}
const initialCode = useSelector(selectCode(worldId, levelId))
const {editor, infoProvider, editorConnection} =
useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
@@ -168,7 +177,7 @@ function Level() {
<EditorContext.Provider value={editorConnection}>
<MonacoEditorContext.Provider value={editor}>
<InputModeContext.Provider value={{commandLineMode, setCommandLineMode}}>
<InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
{editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
</InputModeContext.Provider>
</MonacoEditorContext.Provider>
client/src/components/infoview/CommandLine.tsx
+133 -45
View File
@@ -8,30 +8,108 @@ import { InputModeContext, MonacoEditorContext } from '../Level'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
import { Registry } from 'monaco-textmate' // peer dependency
import { wireTmGrammars } from 'monaco-editor-textmate'
import * as lightPlusTheme from 'lean4web/client/src/lightPlus.json'
import * as leanSyntax from 'lean4web/client/src/syntaxes/lean.json'
import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.json'
import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json'
import languageConfig from 'lean4/language-configuration.json';
function hasErrorsOrWarnings(diags) {
return diags.some(
(d) =>
!d.message.startsWith("unsolved goals") &&
(d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning)
)
}
/* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
// register Monaco languages
monaco.languages.register({
id: 'lean4cmd',
extensions: ['.leancmd']
})
// map of monaco "language id's" to TextMate scopeNames
const grammars = new Map()
grammars.set('lean4', 'source.lean')
grammars.set('lean4cmd', 'source.lean')
const registry = new Registry({
getGrammarDefinition: async (scopeName) => {
if (scopeName === 'source.lean') {
return {
format: 'json',
content: JSON.stringify(leanSyntax)
}
} else if (scopeName === 'source.lean.markdown') {
return {
format: 'json',
content: JSON.stringify(leanMarkdownSyntax)
}
} else {
return {
format: 'json',
content: JSON.stringify(codeblockSyntax)
}
}
}
});
wireTmGrammars(monaco, registry, grammars)
let config: any = { ...languageConfig }
config.autoClosingPairs = config.autoClosingPairs.map(
pair => { return {'open': pair[0], 'close': pair[1]} }
)
monaco.languages.setLanguageConfiguration('lean4cmd', config);
export function CommandLine() {
/** Reference to the hidden multi-line editor */
const editor = React.useContext(MonacoEditorContext)
const commandInput = useRef<HTMLInputElement>()
const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
const [processing, setProcessing] = useState(false)
const { commandLineMode } = React.useContext(InputModeContext)
const allDiags = React.useContext(LspDiagnosticsContext)
const diags = allDiags.get(editor.getModel().uri.toString())
const { commandLineMode, commandLineInput, setCommandLineInput } = React.useContext(InputModeContext)
const inputRef = useRef()
// Run the command
const runCommand = React.useCallback(() => {
if (processing) return;
const pos = editor.getPosition()
editor.executeEdits("command-line", [{
range: monaco.Selection.fromPositions(
pos,
editor.getModel().getFullModelRange().getEndPosition()
),
text: commandLineInput + "\n",
forceMoveMarkers: false
}]);
editor.setPosition(pos)
setProcessing(true)
}, [commandLineInput, editor])
useEffect(() => {
const editor = monaco.editor.create(inputRef.current!, {
if (oneLineEditor && oneLineEditor.getValue() !== commandLineInput) {
oneLineEditor.setValue(commandLineInput)
}
}, [commandLineInput])
// React when answer from the server comes back
useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
if (params.uri == editor.getModel().uri.toString()) {
setProcessing(false)
if (!hasErrorsOrWarnings(params.diagnostics)) {
setCommandLineInput("")
editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
}
}
}, []);
useEffect(() => {
const myEditor = monaco.editor.create(inputRef.current!, {
value: commandLineInput,
language: "lean4cmd",
quickSuggestions: false,
lightbulb: {
enabled: true
@@ -46,30 +124,51 @@ export function CommandLine() {
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'
vertical: 'hidden',
horizontalScrollbarSize: 3
},
overviewRulerBorder: false,
theme: 'vs-code-theme-converted',
contextmenu: false
})
const t = editor.getModel().onDidChangeContent((e) => {
const value = editor.getValue()
setOneLineEditor(myEditor)
const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), myEditor.getModel(), myEditor)
return () => {abbrevRewriter.dispose(); myEditor.dispose()}
}, [])
useEffect(() => {
if (!oneLineEditor) return
// Ensure that our one-line editor can only have a single line
const l = oneLineEditor.getModel().onDidChangeContent((e) => {
const value = oneLineEditor.getValue()
setCommandLineInput(value)
const newValue = value.replace(/[\n\r]/g, '')
if (value != newValue) {
editor.setValue(newValue)
oneLineEditor.setValue(newValue)
}
})
return () => { l.dispose() }
}, [oneLineEditor, setCommandLineInput])
return () => {t.dispose(); editor.dispose()}
}, [])
useEffect(() => {
if (!oneLineEditor) return
// Run command when pressing enter
const l = oneLineEditor.onKeyUp((ev) => {
if (ev.code === "Enter") {
runCommand()
}
})
return () => { l.dispose() }
}, [oneLineEditor, runCommand])
// Effect when command line mode gets enabled
useEffect(() => {
@@ -78,7 +177,7 @@ export function CommandLine() {
if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
editor.executeEdits("command-line", [{
range: monaco.Selection.fromPositions(endPos, endPos),
text: "\n",
text: commandLineInput + "\n",
forceMoveMarkers: false
}]);
}
@@ -86,38 +185,27 @@ export function CommandLine() {
}
}, [commandLineMode])
// Run the command
const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
ev.preventDefault()
const pos = editor.getPosition()
editor.executeEdits("command-line", [{
range: monaco.Selection.fromPositions(
pos,
editor.getModel().getFullModelRange().getEndPosition()
),
text: commandInput.current!.value + "\n",
forceMoveMarkers: false
}]);
editor.setPosition(pos)
setProcessing(true)
runCommand()
}
// React when answer from the server comes back
useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
if (params.uri == editor.getModel().uri.toString()) {
setProcessing(false)
if (!hasErrorsOrWarnings(params.diagnostics)) {
commandInput.current!.value = "";
editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
}
}
}, []);
return <div className="command-line">
<form onSubmit={handleSubmit}>
<div ref={inputRef} className="command-line-input" />
{/* <input type="text" ref={commandInput} disabled={processing} /> */}
<div className="command-line-input-wrapper">
<div ref={inputRef} className="command-line-input" />
</div>
<button type="submit" disabled={processing} className="btn btn-inverted"><FontAwesomeIcon icon={faWandMagicSparkles} /> Run</button>
</form>
</div>
}
/** Checks whether the diagnostics contain any errors or warnings to check whether the level has
been completed.*/
function hasErrorsOrWarnings(diags) {
return diags.some(
(d) =>
!d.message.startsWith("unsolved goals") &&
(d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning)
)
}
client/src/components/infoview/infoview.css
+15 -2
View File
@@ -52,8 +52,21 @@
display: block;
}
.command-line .command-line-input{
.command-line .command-line-input-wrapper{
flex: 1;
padding: 0.2em .6em;
padding: 0.4em .6em 0;
font-size: 1rem;
background: white;
}
.command-line .command-line-input{
height: 1.2em;
}
/* Turn off some monaco decorations: */
.command-line-input .monaco-editor .view-overlays .current-line {
border: 0;
}
.command-line-input .monaco-editor .scroll-decoration {
box-shadow: none;
}
client/src/components/level.css
+21
View File
@@ -117,6 +117,27 @@ td code {
white-space:nowrap;
}
/* Styling in the editor while typing abbreviations such as "\alpha" */
.abbreviation {
text-decoration: underline;
}
/* Styling in the left margin of the editor when processing */
.processing {
background: linear-gradient(
to right,
rgba(255, 165, 0, 1) 0%,
rgba(255, 165, 0, 1) 30%,
transparent 30%,
transparent 100%
);
}
/* Styling in the left margin of the editor on error */
.glyph-margin-error {
background: rgba(255, 0, 0, 1);
}
/***************************************/
/* TODO: For development purposes only */
/***************************************/