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

work on network interruption errors

Browse Source
better-timeout
joneugster 1 year ago
parent 940663f640
commit bea342b2c7
4 changed files with 202 additions and 179 deletions
Show Stats Download Patch File Download Diff File

88
client/src/components/infoview/main.tsx
Unescape Escape View File

@ -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 {

29
client/src/components/infoview/typewriter.tsx
Unescape Escape View File

@ -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) => {

28
client/src/components/inventory.tsx
Unescape Escape View File

@ -115,20 +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>
{doc.status == QueryStatus.fulfilled ?
<>
<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>
</> : <p>Loading...</p>
}
<DocContent doc={doc} />
</div>
}

236
client/src/components/level.tsx
Unescape Escape View File

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

Write Preview
Loading…
Cancel
Save