@@ -338,19 +350,51 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number
return
}
+/** 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
= []
+ 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(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(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 = []
- 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 {
diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx
index 347a0211..2779ee68 100644
--- a/client/src/components/infoview/typewriter.tsx
+++ b/client/src/components/infoview/typewriter.tsx
@@ -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(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 = (ev) => {
diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx
index 896b1f77..25596a17 100644
--- a/client/src/components/inventory.tsx
+++ b/client/src/components/inventory.tsx
@@ -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 {icon} {displayName}
}
+/** Wrapper to catch rejected/pending queries. */
+function DocContent({doc}) {
+ switch(doc.status) {
+ case QueryStatus.fulfilled:
+ return <>
+ {doc.data.displayName}
+ {doc.data.statement}
+ {/* docstring: {doc.data.docstring} */}
+ {doc.data.content}
+
+ case QueryStatus.rejected:
+ return Looks like there is a connection problem!
+ case QueryStatus.pending:
+ return Loading...
+ default:
+ return <>
+ }
+}
+
export function Documentation({name, type, handleClose}) {
const gameId = React.useContext(GameIdContext)
const doc = useLoadDocQuery({game: gameId, type: type, name: name})
return
-
{doc.data?.displayName}
-
{doc.data?.statement}
- {/*
docstring: {doc.data?.docstring} */}
-
{doc.data?.content}
+
}
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 9e969417..a4e93536 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -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()
-
- // 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.`)
+ 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()}`)
+
+
+ // 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 <>
@@ -483,33 +489,9 @@ function Introduction({impressum, setImpressum}) {
}
-
}
-// {mobile?
-// // TODO: This is copied from the `Split` component below...
-// <>
-//
-//
-//
-//
-//
-// :
-//
-//
-//
-//
-//
-// }
-
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])
}