From 940663f6403e01c01cb6495d5208974cfd10bc4e Mon Sep 17 00:00:00 2001 From: joneugster Date: Fri, 27 Oct 2023 18:48:02 +0200 Subject: [PATCH 1/2] improve loading of inventory doc popups #138 --- client/src/components/inventory.tsx | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index 896b1f77..562dbf55 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'; @@ -120,10 +121,14 @@ export function Documentation({name, type, handleClose}) { return
-

{doc.data?.displayName}

-

{doc.data?.statement}

- {/* docstring: {doc.data?.docstring} */} - {doc.data?.content} + {doc.status == QueryStatus.fulfilled ? + <> +

{doc.data.displayName}

+

{doc.data.statement}

+ {/* docstring: {doc.data.docstring} */} + {doc.data.content} + :

Loading...

+ }
} From bea342b2c72fbd93a1eb5405a03d0bf99f6e03bc Mon Sep 17 00:00:00 2001 From: joneugster Date: Fri, 27 Oct 2023 21:02:20 +0200 Subject: [PATCH 2/2] work on network interruption errors --- client/src/components/infoview/main.tsx | 88 ++++--- client/src/components/infoview/typewriter.tsx | 29 ++- client/src/components/inventory.tsx | 28 ++- client/src/components/level.tsx | 236 ++++++++---------- 4 files changed, 202 insertions(+), 179 deletions(-) diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index ab670a12..d587a91f 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -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

no internet?

+ } + } catch { + return

no internet??

+ } + if (!serverVersion) { return <> } if (serverStoppedResult) { return
@@ -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 562dbf55..25596a17 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -115,20 +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.status == QueryStatus.fulfilled ? - <> -

{doc.data.displayName}

-

{doc.data.statement}

- {/* docstring: {doc.data.docstring} */} - {doc.data.content} - :

Loading...

- } +
} 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]) }