Compare commits
2
Commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
bea342b2c7 | ||
|
|
940663f640 |
@@ -1,6 +1,7 @@
|
||||
/* Partly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx */
|
||||
|
||||
import * as React from 'react';
|
||||
import {useEffect} from 'react';
|
||||
import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol';
|
||||
|
||||
import 'tachyons/css/tachyons.css';
|
||||
@@ -327,6 +328,17 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number
|
||||
// it's important not to reconstruct the `WithBlah` wrappers below since they contain state
|
||||
// that we want to persist.
|
||||
|
||||
// Catch loss of internet connection
|
||||
try {
|
||||
const editor = React.useContext(MonacoEditorContext)
|
||||
const model = editor.getModel()
|
||||
if (!model) {
|
||||
return <p>no internet?</p>
|
||||
}
|
||||
} catch {
|
||||
return <p>no internet??</p>
|
||||
}
|
||||
|
||||
if (!serverVersion) { return <></> }
|
||||
if (serverStoppedResult) {
|
||||
return <div>
|
||||
@@ -338,19 +350,51 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number
|
||||
return <TypewriterInterface props={props} />
|
||||
}
|
||||
|
||||
/** Delete all proof lines starting from a given line.
|
||||
* Note that the first line (i.e. deleting everything) is `1`!
|
||||
*/
|
||||
function deleteProof(line: number) {
|
||||
const editor = React.useContext(MonacoEditorContext)
|
||||
const { proof } = React.useContext(ProofContext)
|
||||
const { setSelectedStep } = React.useContext(SelectionContext)
|
||||
const { setDeletedChat, showHelp } = React.useContext(DeletedChatContext)
|
||||
const { setTypewriterInput } = React.useContext(InputModeContext)
|
||||
|
||||
return (ev) => {
|
||||
if (editor) {
|
||||
const model = editor.getModel()
|
||||
if (model) {
|
||||
let deletedChat: Array<GameHint> = []
|
||||
proof.slice(line).map((step, i) => {
|
||||
// Only add these hidden hints to the deletion stack which were visible
|
||||
deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
|
||||
})
|
||||
setDeletedChat(deletedChat)
|
||||
editor.executeEdits("typewriter", [{
|
||||
range: monaco.Selection.fromPositions(
|
||||
{ lineNumber: line, column: 1 },
|
||||
model.getFullModelRange().getEndPosition()
|
||||
),
|
||||
text: '',
|
||||
forceMoveMarkers: false
|
||||
}])
|
||||
setSelectedStep(undefined)
|
||||
setTypewriterInput(proof[line].command)
|
||||
ev.stopPropagation()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/** The interface in command line mode */
|
||||
export function TypewriterInterface({props}) {
|
||||
const ec = React.useContext(EditorContext)
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const editor = React.useContext(MonacoEditorContext)
|
||||
const model = editor.getModel()
|
||||
const uri = model.uri.toString()
|
||||
|
||||
const [disableInput, setDisableInput] = React.useState<boolean>(false)
|
||||
const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
|
||||
const { showHelp, setShowHelp } = React.useContext(DeletedChatContext)
|
||||
const {mobile} = React.useContext(MobileContext)
|
||||
const { proof } = React.useContext(ProofContext)
|
||||
const { setTypewriterInput } = React.useContext(InputModeContext)
|
||||
const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
|
||||
|
||||
const proofPanelRef = React.useRef<HTMLDivElement>(null)
|
||||
@@ -358,33 +402,9 @@ export function TypewriterInterface({props}) {
|
||||
// const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
|
||||
// const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
|
||||
|
||||
const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
|
||||
|
||||
/** Delete all proof lines starting from a given line.
|
||||
* Note that the first line (i.e. deleting everything) is `1`!
|
||||
*/
|
||||
function deleteProof(line: number) {
|
||||
return (ev) => {
|
||||
let deletedChat: Array<GameHint> = []
|
||||
proof.slice(line).map((step, i) => {
|
||||
// Only add these hidden hints to the deletion stack which were visible
|
||||
deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
|
||||
})
|
||||
setDeletedChat(deletedChat)
|
||||
|
||||
editor.executeEdits("typewriter", [{
|
||||
range: monaco.Selection.fromPositions(
|
||||
{ lineNumber: line, column: 1 },
|
||||
editor.getModel().getFullModelRange().getEndPosition()
|
||||
),
|
||||
text: '',
|
||||
forceMoveMarkers: false
|
||||
}])
|
||||
setSelectedStep(undefined)
|
||||
setTypewriterInput(proof[line].command)
|
||||
ev.stopPropagation()
|
||||
}
|
||||
}
|
||||
// rpc session
|
||||
// editor, model or uri might be null if connection is broken
|
||||
const rpcSess = useRpcSessionAtPos({uri: editor?.getModel()?.uri?.toString() ?? '', line: 0, character: 0})
|
||||
|
||||
function toggleSelectStep(line: number) {
|
||||
return (ev) => {
|
||||
@@ -399,8 +419,8 @@ export function TypewriterInterface({props}) {
|
||||
}
|
||||
}
|
||||
|
||||
// Scroll to the end of the proof if it is updated.
|
||||
React.useEffect(() => {
|
||||
// Scroll to the end of the proof if it is updated.
|
||||
React.useEffect(() => {
|
||||
if (proof?.length > 1) {
|
||||
proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
|
||||
} else {
|
||||
|
||||
@@ -68,8 +68,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
|
||||
/** Reference to the hidden multi-line editor */
|
||||
const editor = React.useContext(MonacoEditorContext)
|
||||
const model = editor.getModel()
|
||||
const uri = model.uri.toString()
|
||||
const model = editor?.getModel()
|
||||
const uri = model?.uri?.toString()
|
||||
|
||||
const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
|
||||
const [processing, setProcessing] = useState(false)
|
||||
@@ -91,11 +91,15 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
*/
|
||||
const loadAllGoals = React.useCallback(() => {
|
||||
|
||||
if (!model || ! uri) {
|
||||
return
|
||||
}
|
||||
|
||||
let goalCalls = []
|
||||
let msgCalls = []
|
||||
|
||||
// For each line of code ask the server for the goals and the messages on this line
|
||||
for (let i = 0; i < model.getLineCount(); i++) {
|
||||
for (let i = 0; i < model?.getLineCount(); i++) {
|
||||
goalCalls.push(
|
||||
rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
|
||||
)
|
||||
@@ -158,7 +162,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
// with no goals there will be no hints.
|
||||
let hints : GameHint[] = goals.goals.length ? goals.goals[0].hints : []
|
||||
|
||||
console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
|
||||
console.debug(`Command (${i}): `, i ? model?.getLineContent(i) : '')
|
||||
console.debug(`Goals: (${i}): `, goalsToString(goals)) //
|
||||
console.debug(`Hints: (${i}): `, hints)
|
||||
console.debug(`Errors: (${i}): `, messages)
|
||||
@@ -166,7 +170,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
tmpProof.push({
|
||||
// the command of the line above. Note that `getLineContent` starts counting
|
||||
// at `1` instead of `zero`. The first ProofStep will have an empty command.
|
||||
command: i ? model.getLineContent(i) : '',
|
||||
command: i ? model?.getLineContent(i) : '',
|
||||
// TODO: store correct data
|
||||
goals: goals.goals,
|
||||
// only need the hints of the active goals in chat
|
||||
@@ -185,6 +189,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
// Run the command
|
||||
const runCommand = React.useCallback(() => {
|
||||
if (processing) {return}
|
||||
if (!uri) {return}
|
||||
|
||||
// TODO: Desired logic is to only reset this after a new *error-free* command has been entered
|
||||
setDeletedChat([])
|
||||
@@ -195,7 +200,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
editor.executeEdits("typewriter", [{
|
||||
range: monaco.Selection.fromPositions(
|
||||
pos,
|
||||
editor.getModel().getFullModelRange().getEndPosition()
|
||||
model.getFullModelRange().getEndPosition()
|
||||
),
|
||||
text: typewriterInput.trim() + "\n",
|
||||
forceMoveMarkers: false
|
||||
@@ -204,7 +209,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
}
|
||||
|
||||
editor.setPosition(pos)
|
||||
}, [typewriterInput, editor])
|
||||
}, [typewriterInput, editor, model])
|
||||
|
||||
useEffect(() => {
|
||||
if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
|
||||
@@ -220,12 +225,14 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
|
||||
// React when answer from the server comes back
|
||||
useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
|
||||
if (!uri) {return}
|
||||
|
||||
if (params.uri == uri) {
|
||||
setProcessing(false)
|
||||
loadAllGoals()
|
||||
if (!hasErrors(params.diagnostics)) {
|
||||
//setTypewriterInput("")
|
||||
editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
|
||||
editor.setPosition(model.getFullModelRange().getEndPosition())
|
||||
}
|
||||
} else {
|
||||
// console.debug(`expected uri: ${uri}, got: ${params.uri}`)
|
||||
@@ -234,7 +241,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
// TODO: This is the wrong place apparently. Where do wee need to load them?
|
||||
// TODO: instead of loading all goals every time, we could only load the last one
|
||||
// loadAllGoals()
|
||||
}, [uri]);
|
||||
}, [uri, editor, model]);
|
||||
|
||||
useEffect(() => {
|
||||
const myEditor = monaco.editor.create(inputRef.current!, {
|
||||
@@ -304,10 +311,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
|
||||
// BUG: Causes `file closed` error
|
||||
//TODO: Intention is to run once when loading, does that work?
|
||||
useEffect(() => {
|
||||
console.debug(`time to update: ${uri} \n ${rpcSess}`)
|
||||
console.debug(rpcSess)
|
||||
loadAllGoals()
|
||||
}, [rpcSess])
|
||||
}, [])
|
||||
|
||||
/** Process the entered command */
|
||||
const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
|
||||
|
||||
@@ -6,6 +6,7 @@ import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
|
||||
import { GameIdContext } from '../app';
|
||||
import Markdown from './markdown';
|
||||
import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
|
||||
import { QueryStatus } from '@reduxjs/toolkit/query/react'
|
||||
import { selectDifficulty, selectInventory } from '../state/progress';
|
||||
import { store } from '../state/store';
|
||||
import { useSelector } from 'react-redux';
|
||||
@@ -114,16 +115,32 @@ function InventoryItem({name, displayName, locked, disabled, newly, showDoc, ena
|
||||
return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>{icon} {displayName}</div>
|
||||
}
|
||||
|
||||
/** Wrapper to catch rejected/pending queries. */
|
||||
function DocContent({doc}) {
|
||||
switch(doc.status) {
|
||||
case QueryStatus.fulfilled:
|
||||
return <>
|
||||
<h1 className="doc">{doc.data.displayName}</h1>
|
||||
<p><code>{doc.data.statement}</code></p>
|
||||
{/* <code>docstring: {doc.data.docstring}</code> */}
|
||||
<Markdown>{doc.data.content}</Markdown>
|
||||
</>
|
||||
case QueryStatus.rejected:
|
||||
return <p>Looks like there is a connection problem!</p>
|
||||
case QueryStatus.pending:
|
||||
return <p>Loading...</p>
|
||||
default:
|
||||
return <></>
|
||||
}
|
||||
}
|
||||
|
||||
export function Documentation({name, type, handleClose}) {
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const doc = useLoadDocQuery({game: gameId, type: type, name: name})
|
||||
|
||||
return <div className="documentation">
|
||||
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
|
||||
<h1 className="doc">{doc.data?.displayName}</h1>
|
||||
<p><code>{doc.data?.statement}</code></p>
|
||||
{/* <code>docstring: {doc.data?.docstring}</code> */}
|
||||
<Markdown>{doc.data?.content}</Markdown>
|
||||
<DocContent doc={doc} />
|
||||
</div>
|
||||
}
|
||||
|
||||
|
||||
+108
-122
@@ -237,8 +237,6 @@ function PlayableLevel({impressum, setImpressum}) {
|
||||
const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
|
||||
function closeInventoryDoc () {setInventoryDoc(null)}
|
||||
|
||||
|
||||
|
||||
const onDidChangeContent = (code) => {
|
||||
dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code}))
|
||||
}
|
||||
@@ -254,30 +252,30 @@ function PlayableLevel({impressum, setImpressum}) {
|
||||
const {editor, infoProvider, editorConnection} =
|
||||
useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection)
|
||||
|
||||
/** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
|
||||
* `TypewriterInterface`.
|
||||
*/
|
||||
const handleUndo = () => {
|
||||
const endPos = editor.getModel().getFullModelRange().getEndPosition()
|
||||
let range
|
||||
console.log(endPos.column)
|
||||
if (endPos.column === 1) {
|
||||
range = monaco.Selection.fromPositions(
|
||||
new monaco.Position(endPos.lineNumber - 1, 1),
|
||||
endPos
|
||||
)
|
||||
} else {
|
||||
range = monaco.Selection.fromPositions(
|
||||
new monaco.Position(endPos.lineNumber, 1),
|
||||
endPos
|
||||
)
|
||||
}
|
||||
editor.executeEdits("undo-button", [{
|
||||
range,
|
||||
text: "",
|
||||
forceMoveMarkers: false
|
||||
}]);
|
||||
}
|
||||
// /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
|
||||
// * `TypewriterInterface`.
|
||||
// */
|
||||
// const handleUndo = () => {
|
||||
// const endPos = editor.getModel().getFullModelRange().getEndPosition()
|
||||
// let range
|
||||
// console.log(endPos.column)
|
||||
// if (endPos.column === 1) {
|
||||
// range = monaco.Selection.fromPositions(
|
||||
// new monaco.Position(endPos.lineNumber - 1, 1),
|
||||
// endPos
|
||||
// )
|
||||
// } else {
|
||||
// range = monaco.Selection.fromPositions(
|
||||
// new monaco.Position(endPos.lineNumber, 1),
|
||||
// endPos
|
||||
// )
|
||||
// }
|
||||
// editor.executeEdits("undo-button", [{
|
||||
// range,
|
||||
// text: "",
|
||||
// forceMoveMarkers: false
|
||||
// }]);
|
||||
// }
|
||||
|
||||
// Select and highlight proof steps and corresponding hints
|
||||
// TODO: with the new design, there is no difference between the introduction and
|
||||
@@ -296,28 +294,31 @@ function PlayableLevel({impressum, setImpressum}) {
|
||||
setTypewriterMode(false)
|
||||
|
||||
if (editor) {
|
||||
let code = editor.getModel().getLinesContent()
|
||||
let model = editor.getModel()
|
||||
if (model) {
|
||||
let code = model.getLinesContent()
|
||||
|
||||
// console.log(`insert. code: ${code}`)
|
||||
// console.log(`insert. join: ${code.join('')}`)
|
||||
// console.log(`insert. trim: ${code.join('').trim()}`)
|
||||
// console.log(`insert. length: ${code.join('').trim().length}`)
|
||||
// console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
|
||||
// console.log(`insert. code: ${code}`)
|
||||
// console.log(`insert. join: ${code.join('')}`)
|
||||
// console.log(`insert. trim: ${code.join('').trim()}`)
|
||||
// console.log(`insert. length: ${code.join('').trim().length}`)
|
||||
// console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
|
||||
|
||||
|
||||
// TODO: It does seem that the template is always indented by spaces.
|
||||
// This is a hack, assuming there are exactly two.
|
||||
if (!code.join('').trim().length) {
|
||||
console.debug(`inserting template:\n${level.data.template}`)
|
||||
// TODO: This does not work! HERE
|
||||
// Probably overwritten by a query to the server
|
||||
editor.executeEdits("template-writer", [{
|
||||
range: editor.getModel().getFullModelRange(),
|
||||
text: level.data.template + `\n`,
|
||||
forceMoveMarkers: true
|
||||
}])
|
||||
} else {
|
||||
console.debug(`not inserting template.`)
|
||||
// TODO: It does seem that the template is always indented by spaces.
|
||||
// This is a hack, assuming there are exactly two.
|
||||
if (!code.join('').trim().length) {
|
||||
console.debug(`inserting template:\n${level.data.template}`)
|
||||
// TODO: This does not work! HERE
|
||||
// Probably overwritten by a query to the server
|
||||
editor.executeEdits("template-writer", [{
|
||||
range: model.getFullModelRange(),
|
||||
text: level.data.template + `\n`,
|
||||
forceMoveMarkers: true
|
||||
}])
|
||||
} else {
|
||||
console.debug(`not inserting template.`)
|
||||
}
|
||||
}
|
||||
}
|
||||
} else {
|
||||
@@ -335,17 +336,49 @@ function PlayableLevel({impressum, setImpressum}) {
|
||||
setShowHelp(new Set(selectHelp(gameId, worldId, levelId)(store.getState())))
|
||||
}, [gameId, worldId, levelId])
|
||||
|
||||
// switching editor mode
|
||||
useEffect(() => {
|
||||
if (!typewriterMode) {
|
||||
// Delete last input attempt from command line
|
||||
editor.executeEdits("typewriter", [{
|
||||
range: editor.getSelection(),
|
||||
text: "",
|
||||
forceMoveMarkers: false
|
||||
}]);
|
||||
editor.focus()
|
||||
if (editor) {
|
||||
let model = editor.getModel()
|
||||
if (model) {
|
||||
if (typewriterMode) {
|
||||
// typewriter gets enabled
|
||||
let code = model.getLinesContent().filter(line => line.trim())
|
||||
editor.executeEdits("typewriter", [{
|
||||
range: model.getFullModelRange(),
|
||||
text: code.length ? code.join('\n') + '\n' : '',
|
||||
forceMoveMarkers: true
|
||||
}])
|
||||
|
||||
// let endPos = model.getFullModelRange().getEndPosition()
|
||||
// if (model.getLineContent(endPos.lineNumber).trim() !== "") {
|
||||
// editor.executeEdits("typewriter", [{
|
||||
// range: monaco.Selection.fromPositions(endPos, endPos),
|
||||
// text: "\n",
|
||||
// forceMoveMarkers: true
|
||||
// }]);
|
||||
// }
|
||||
// let endPos = model.getFullModelRange().getEndPosition()
|
||||
// let currPos = editor.getPosition()
|
||||
// if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
|
||||
// // This is not a position that would naturally occur from Typewriter, reset:
|
||||
// editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
|
||||
// }
|
||||
} else {
|
||||
// typewriter gets disabled
|
||||
// delete last input attempt from command line
|
||||
editor.executeEdits("typewriter", [{
|
||||
range: editor.getSelection(),
|
||||
text: "",
|
||||
forceMoveMarkers: false
|
||||
}]);
|
||||
editor.focus()
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
}, [typewriterMode])
|
||||
}, [editor, typewriterMode])
|
||||
|
||||
useEffect(() => {
|
||||
// Forget whether hidden hints are displayed for steps that don't exist yet
|
||||
@@ -363,33 +396,6 @@ function PlayableLevel({impressum, setImpressum}) {
|
||||
}
|
||||
}, [showHelp])
|
||||
|
||||
// Effect when command line mode gets enabled
|
||||
useEffect(() => {
|
||||
if (editor && typewriterMode) {
|
||||
let code = editor.getModel().getLinesContent().filter(line => line.trim())
|
||||
editor.executeEdits("typewriter", [{
|
||||
range: editor.getModel().getFullModelRange(),
|
||||
text: code.length ? code.join('\n') + '\n' : '',
|
||||
forceMoveMarkers: true
|
||||
}]);
|
||||
|
||||
// let endPos = editor.getModel().getFullModelRange().getEndPosition()
|
||||
// if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
|
||||
// editor.executeEdits("typewriter", [{
|
||||
// range: monaco.Selection.fromPositions(endPos, endPos),
|
||||
// text: "\n",
|
||||
// forceMoveMarkers: true
|
||||
// }]);
|
||||
// }
|
||||
// let endPos = editor.getModel().getFullModelRange().getEndPosition()
|
||||
// let currPos = editor.getPosition()
|
||||
// if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
|
||||
// // This is not a position that would naturally occur from Typewriter, reset:
|
||||
// editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
|
||||
// }
|
||||
}
|
||||
}, [editor, typewriterMode])
|
||||
|
||||
return <>
|
||||
<div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
|
||||
<DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
|
||||
@@ -483,33 +489,9 @@ function Introduction({impressum, setImpressum}) {
|
||||
<InventoryPanel levelInfo={inventory?.data} />
|
||||
</Split>
|
||||
}
|
||||
|
||||
</>
|
||||
}
|
||||
|
||||
// {mobile?
|
||||
// // TODO: This is copied from the `Split` component below...
|
||||
// <>
|
||||
// <div className={`app-content level-mobile ${level.isLoading ? 'hidden' : ''}`}>
|
||||
// <ExercisePanel
|
||||
// impressum={impressum}
|
||||
// closeImpressum={closeImpressum}
|
||||
// codeviewRef={codeviewRef}
|
||||
// visible={pageNumber == 0} />
|
||||
// <InventoryPanel levelInfo={level?.data} visible={pageNumber == 1} />
|
||||
// </div>
|
||||
// </>
|
||||
// :
|
||||
// <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
|
||||
// <ChatPanel lastLevel={lastLevel}/>
|
||||
// <ExercisePanel
|
||||
// impressum={impressum}
|
||||
// closeImpressum={closeImpressum}
|
||||
// codeviewRef={codeviewRef} />
|
||||
// <InventoryPanel levelInfo={level?.data} />
|
||||
// </Split>
|
||||
// }
|
||||
|
||||
function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
|
||||
|
||||
const connection = React.useContext(ConnectionContext)
|
||||
@@ -604,18 +586,20 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
|
||||
if (!model) {
|
||||
model = monaco.editor.createModel(initialCode, 'lean4', uri)
|
||||
}
|
||||
model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
|
||||
editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
|
||||
editor.setModel(model)
|
||||
if (initialSelections) {
|
||||
console.debug("Initial Selection: ", initialSelections)
|
||||
// BUG: Somehow I get an `invalid arguments` bug here
|
||||
// editor.setSelections(initialSelections)
|
||||
}
|
||||
if (model) { // in case of broken pipe, this remains null
|
||||
model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
|
||||
editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
|
||||
editor.setModel(model)
|
||||
if (initialSelections) {
|
||||
console.debug("Initial Selection: ", initialSelections)
|
||||
// BUG: Somehow I get an `invalid arguments` bug here
|
||||
// editor.setSelections(initialSelections)
|
||||
}
|
||||
|
||||
return () => {
|
||||
editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
|
||||
model.dispose(); }
|
||||
return () => {
|
||||
editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
|
||||
model.dispose(); }
|
||||
}
|
||||
}
|
||||
}, [editor, levelId, connection, leanClientStarted])
|
||||
|
||||
@@ -624,14 +608,16 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
|
||||
if (editor && leanClientStarted) {
|
||||
|
||||
let model = monaco.editor.getModel(uri)
|
||||
infoviewApi.serverRestarted(leanClient.initializeResult)
|
||||
if (model) {
|
||||
infoviewApi.serverRestarted(leanClient.initializeResult)
|
||||
|
||||
infoProvider.openPreview(editor, infoviewApi)
|
||||
infoProvider.openPreview(editor, infoviewApi)
|
||||
|
||||
const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
|
||||
const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
|
||||
const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
|
||||
const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
|
||||
|
||||
return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
|
||||
return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
|
||||
}
|
||||
}
|
||||
}, [editor, connection, leanClientStarted])
|
||||
|
||||
@@ -657,7 +643,7 @@ function useLoadWorldFiles(worldId) {
|
||||
models.push(monaco.editor.createModel(code, 'lean4', uri))
|
||||
}
|
||||
}
|
||||
return () => { for (let model of models) { model.dispose() } }
|
||||
return () => { for (let model of models) { try {model.dispose()} catch {console.log(`failed to dispose model ${model}`)}} }
|
||||
}
|
||||
}, [gameInfo.data, worldId])
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user