diff --git a/client/src/components/chat.tsx b/client/src/components/chat.tsx index ec4c715..bcca2c3 100644 --- a/client/src/components/chat.tsx +++ b/client/src/components/chat.tsx @@ -11,11 +11,11 @@ import { useAppDispatch, useAppSelector } from '../hooks' import { Button, Markdown } from './utils' import { ChatContext, GameIdContext, PageContext, PreferencesContext, ProofContext } from '../state/context' import { GameHint, InteractiveGoalsWithHints } from './infoview/rpc_api' -import { lastStepHasErrors } from './infoview/goals' -import { AllMessages } from '../../../node_modules/@leanprover/infoview/dist/infoview/messages' -import { LeanDiagnostic, RpcErrorCode, getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api' +// import { lastStepHasErrors } from './infoview/goals' +// import { AllMessages } from '../../../node_modules/@leanprover/infoview/dist/infoview/messages' +// import { LeanDiagnostic, RpcErrorCode, getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api' import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol' -import { InteractiveMessage } from '../../../node_modules/lean4-infoview/src/infoview/traceExplorer' +// import { InteractiveMessage } from '../../../node_modules/lean4-infoview/src/infoview/traceExplorer' import '../css/chat.css' import { faHome } from '@fortawesome/free-solid-svg-icons' @@ -39,9 +39,10 @@ export function MoreHelpButton({selected=null} : {selected?: number}) { const { proof } = React.useContext(ProofContext) const { showHelp, setShowHelp } = React.useContext(ChatContext) - let k = proof?.steps.length ? - ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected) - : 0 + let k = 0 + // let k = proof?.steps.length ? + // ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected) + // : 0 const activateHiddenHints = (ev) => { // If the last step (`k`) has errors, we want the hidden hints from the @@ -204,10 +205,10 @@ export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[ } // TODO -function helper(step, proof, kind, typewriterMode, selectedStep) { - return (step == proof?.steps?.length - (lastStepHasErrors(proof) ? 2 : 1) ? ' recent' : '') + - (!(kind == HintKind.Conclusion) && step >= (typewriterMode ? proof?.steps?.length : selectedStep+1) ? ' deleted-hint' : '') -} +// function helper(step, proof, kind, typewriterMode, selectedStep) { +// return (step == proof?.steps?.length - (lastStepHasErrors(proof) ? 2 : 1) ? ' recent' : '') + +// (!(kind == HintKind.Conclusion) && step >= (typewriterMode ? proof?.steps?.length : selectedStep+1) ? ' deleted-hint' : '') +// } /** A hint as it is displayed in the chat. */ export function Hint({hint, kind, step=null} : GameHintWithStep) { @@ -232,7 +233,7 @@ export function Hint({hint, kind, step=null} : GameHintWithStep) { // until the next command is submitted; in editor, moving the cursor through the proof will // render all hints return
{getHintText(hint)}
@@ -350,7 +351,7 @@ export function ChatPanel ({visible = true}) { chatRef.current!.lastElementChild?.scrollIntoView({block: "center"}) } else { // proof currently not completed: first message of last step - let lastStep = proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) + let lastStep = proof?.steps.length //- (lastStepHasErrors(proof) ? 2 : 1) console.debug(`scroll chat: first message of step ${lastStep}`) chatRef.current?.getElementsByClassName(`step-${lastStep}`)[0]?.scrollIntoView({block: "center"}) } @@ -369,7 +370,7 @@ export function ChatPanel ({visible = true}) { // Scroll down when new hidden hints are triggered useEffect(() => { if (levelId > 0) { - let lastStep = proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) + let lastStep = proof?.steps.length //- (lastStepHasErrors(proof) ? 2 : 1) if (showHelp.has(lastStep)) { console.debug('scroll chat: down to hidden hints') // TODO: last element of hidden hints? diff --git a/client/src/components/editor.tsx b/client/src/components/editor.tsx deleted file mode 100644 index ee5ace7..0000000 --- a/client/src/components/editor.tsx +++ /dev/null @@ -1,7 +0,0 @@ -import * as React from 'react' - -export function Editor () { - return

- I'm an editor -

-} diff --git a/client/src/components/editor/Editor.tsx b/client/src/components/editor/Editor.tsx new file mode 100644 index 0000000..1933c71 --- /dev/null +++ b/client/src/components/editor/Editor.tsx @@ -0,0 +1,93 @@ +import * as React from 'react'; +import Split from 'react-split' +import { useContext, useEffect, useRef, useState } from 'react' +import { useTranslation } from "react-i18next" +import { GameIdContext } from '../../state/context'; +import { useLoadLevelQuery } from '../../state/api'; +import { Markdown } from '../utils'; +import * as monaco from 'monaco-editor' +import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco' + +import '../../css/editor.css' +import { useSelector } from 'react-redux'; +import { selectTypewriterMode } from '../../state/progress'; + +export function Editor() { + let { t } = useTranslation() + const {gameId, worldId, levelId } = useContext(GameIdContext) + + const typewriterMode = useSelector(selectTypewriterMode(gameId)) + + const editorRef = useRef(null) + const infoviewRef = useRef(null) + const [editor, setEditor] = useState() + const [leanMonaco, setLeanMonaco] = useState() + const [code, setCode] = useState('') + + const [options, setOptions] = useState({ + // placeholder. gets set below + websocket: { + url: '' + } + }) + + // Update LeanMonaco options when preferences are loaded or change + useEffect(() => { + var socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + + window.location.host + `/websocket/${gameId}` + console.log(`[LeanGame] socket url: ${socketUrl}`) + var _options: LeanMonacoOptions = { + websocket: {url: socketUrl}, + // Restrict monaco's extend (e.g. context menu) to the editor itself + htmlElement: editorRef.current ?? undefined, + vscode: { + /* To add settings here, you can open your settings in VSCode (Ctrl+,), search + * for the desired setting, select "Copy Setting as JSON" from the "More Actions" + * menu next to the selected setting, and paste the copied string here. + */ + // "workbench.colorTheme": preferences.theme, + "editor.tabSize": 2, + // "editor.rulers": [100], + "editor.lightbulb.enabled": "on", + "editor.wordWrap": "on", + "editor.wrappingStrategy": "advanced", + "editor.semanticHighlighting.enabled": true, + "editor.acceptSuggestionOnEnter": "off", + "lean4.input.eagerReplacementEnabled": true, + // "lean4.input.leader": preferences.abbreviationCharacter + } + } + setOptions(_options) + }, [editorRef]) + + // Setting up the editor and infoview + useEffect(() => { + console.debug('[LeanGame] Restarting Editor!') + var _leanMonaco = new LeanMonaco() + var leanMonacoEditor = new LeanMonacoEditor() + + _leanMonaco.setInfoviewElement(infoviewRef.current!) + ;(async () => { + await _leanMonaco.start(options) + await leanMonacoEditor.start(editorRef.current!, `${gameId}/${worldId}/Level_${levelId}.lean`, code) + + setEditor(leanMonacoEditor.editor) + setLeanMonaco(_leanMonaco) + + // Keeping the `code` state up-to-date with the changes in the editor + leanMonacoEditor.editor?.onDidChangeModelContent(() => { + setCode(leanMonacoEditor.editor?.getModel()?.getValue()!) + }) + })() + return () => { + leanMonacoEditor.dispose() + _leanMonaco.dispose() + } + }, [options, infoviewRef, editorRef, gameId, worldId, levelId]) + + return +
+
+ +} diff --git a/client/src/components/editor/ExcerciseStatement.tsx b/client/src/components/editor/ExcerciseStatement.tsx new file mode 100644 index 0000000..987f3b6 --- /dev/null +++ b/client/src/components/editor/ExcerciseStatement.tsx @@ -0,0 +1,37 @@ +import * as React from 'react'; +import { useContext, useEffect, useRef, useState } from 'react' +import { useTranslation } from "react-i18next" +import { GameIdContext } from '../../state/context'; +import { useLoadLevelQuery } from '../../state/api'; +import { Markdown } from '../utils'; + +/** The mathematical formulation of the statement, supporting e.g. Latex + * It takes three forms, depending on the precence of name and description: + * - Theorem xyz: description + * - Theorem xyz + * - Exercises: description + * + * If `showLeanStatement` is true, it will additionally display the lean code. + */ +export function ExerciseStatement({ showLeanStatement = false }) { + let { t } = useTranslation() + const {gameId, worldId, levelId } = useContext(GameIdContext) + const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + + if (!(levelInfo.data?.descrText || levelInfo.data?.descrFormat)) { return <> } + return <> +
+ {levelInfo.data?.descrText ? + + {(levelInfo.data?.displayName ? `**${t("Theorem")}** \`${levelInfo.data?.displayName}\`: ` : '') + t(levelInfo.data?.descrText, {ns: gameId})} + : levelInfo.data?.displayName && + + {`**${t("Theorem")}** \`${levelInfo.data?.displayName}\``} + + } + {levelInfo.data?.descrFormat && showLeanStatement && +

{levelInfo.data?.descrFormat}

+ } +
+ +} diff --git a/client/src/components/game.tsx b/client/src/components/game.tsx index b20cba6..1ae1d89 100644 --- a/client/src/components/game.tsx +++ b/client/src/components/game.tsx @@ -11,7 +11,7 @@ import { WorldTreePanel } from './world_tree' import i18next from 'i18next' import { ChatPanel } from './chat' -import { LevelWrapper } from './level' +import { NewLevel } from './level' import { GameHint, ProofState } from './infoview/rpc_api' import { useSelector } from 'react-redux' import { Diagnostic } from 'vscode-languageserver-types' @@ -54,7 +54,6 @@ function Game() { const [interimDiags, setInterimDiags] = useState>([]) const [isCrashed, setIsCrashed] = useState(false) - const typewriterMode = useSelector(selectTypewriterMode(gameId)) const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode})) @@ -83,7 +82,7 @@ function Game() { {<> { worldId ? - : + : } @@ -95,10 +94,12 @@ function Game() {
{/* Note: apparently without this `div` the split panel bugs out. */} - {worldId ? : } + {worldId ? + + : }
- + } diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index 14ea2ae..b9fefa6 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -1,382 +1,382 @@ -/** - * @fileOverview - * - * Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx - */ -import * as React from 'react' -import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api' -import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; -import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'; -import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode' -import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips'; -import { PageContext } from '../../state/context'; -import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api'; -import { RpcSessionAtPos } from '@leanprover/infoview/*'; -import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; -import { DiagnosticSeverity } from 'vscode-languageserver-protocol'; -import { useTranslation } from 'react-i18next'; - -/** Returns true if `h` is inaccessible according to Lean's default name rendering. */ -function isInaccessibleName(h: string): boolean { - return h.indexOf('✝') >= 0; -} - -function goalToString(g: InteractiveGoal): string { - let ret = '' - - if (g.userName) { - ret += `case ${g.userName}\n` - } - - for (const h of g.hyps) { - const names = InteractiveHypothesisBundle_nonAnonymousNames(h).join(' ') - ret += `${names} : ${TaggedText_stripTags(h.type)}` - if (h.val) { - ret += ` := ${TaggedText_stripTags(h.val)}` - } - ret += '\n' - } - - ret += `⊢ ${TaggedText_stripTags(g.type)}` - - return ret -} - -export function goalsToString(goals: InteractiveGoals): string { - return goals.goals.map(g => goalToString(g)).join('\n\n') -} - -export function goalsWithHintsToString(goals: InteractiveGoalsWithHints): string { - return goals.goals.map(g => goalToString(g.goal)).join('\n\n') -} - -interface GoalFilterState { - /** If true reverse the list of hypotheses, if false present the order received from LSP. */ - reverse: boolean, - /** If true show hypotheses that have isType=True, otherwise hide them. */ - showType: boolean, - /** If true show hypotheses that have isInstance=True, otherwise hide them. */ - showInstance: boolean, - /** If true show hypotheses that contain a dagger in the name, otherwise hide them. */ - showHiddenAssumption: boolean - /** If true show the bodies of let-values, otherwise hide them. */ - showLetValue: boolean; -} - -function getFilteredHypotheses(hyps: InteractiveHypothesisBundle[], filter: GoalFilterState): InteractiveHypothesisBundle[] { - return hyps.reduce((acc: InteractiveHypothesisBundle[], h) => { - if (h.isInstance && !filter.showInstance) return acc - if (h.isType && !filter.showType) return acc - const names = filter.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n)) - const hNew: InteractiveHypothesisBundle = filter.showLetValue ? { ...h, names } : { ...h, names, val: undefined } - if (names.length !== 0) acc.push(hNew) - return acc - }, []) -} - -interface HypProps { - hyp: InteractiveHypothesisBundle - mvarId?: MVarId -} - -function Hyp({ hyp: h, mvarId }: HypProps) { - const locs = React.useContext(LocationsContext) - - const namecls: string = 'mr1 ' + - (h.isInserted ? 'inserted-text ' : '') + - (h.isRemoved ? 'removed-text ' : '') - - const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) => - - i ? - { mvarId, loc: { hyp: h.fvarIds[i] }} : - undefined - } - alwaysHighlight={false} - >{n} - ) - - const typeLocs: Locations | undefined = React.useMemo(() => - locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ? - { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds[0], ''] }}} : - undefined, - [locs, mvarId, h.fvarIds]) - - const valLocs: Locations | undefined = React.useMemo(() => - h.val && locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ? - { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds[0], ''] }}} : - undefined, - [h.val, locs, mvarId, h.fvarIds]) - - return
- {names} - :  - - - - {h.val && - -  :=  - } -
-} - -interface GoalProps2 { - goals: InteractiveGoal[] - filter: GoalFilterState -} - -interface GoalProps { - goal: InteractiveGoal - filter: GoalFilterState - showHints?: boolean - typewriter: boolean - unbundle?: boolean /** unbundle `x y : Nat` into `x : Nat` and `y : Nat` */ -} - -/** - * Displays the hypotheses, target type and optional case label of a goal according to the - * provided `filter`. */ -export const Goal = React.memo((props: GoalProps) => { - const { goal, filter, showHints, typewriter, unbundle } = props - let { t } = useTranslation() - - // TODO: Apparently `goal` can be `undefined` - if (!goal) {return <>} - - const filteredList = getFilteredHypotheses(goal.hyps, filter); - const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList; - const locs = React.useContext(LocationsContext) - const goalLocs = React.useMemo(() => - locs && goal.mvarId ? - { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} : - undefined, - [locs, goal.mvarId]) - const goalLi =
- {/*
{t("Goal")}:
*/} - - - -
- - // let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent ' - // if (props.goal.isInserted) cn += 'b--inserted ' - // if (props.goal.isRemoved) cn += 'b--removed ' - - function unbundleHyps (hyps: InteractiveHypothesisBundle[]) : InteractiveHypothesisBundle[] { - return hyps.flatMap(hyp => ( - unbundle ? hyp.names.map(name => {return {...hyp, names: [name]}}) : [hyp] - )) - } - - // const hints = - const objectHyps = unbundleHyps(hyps.filter(hyp => !hyp.isAssumption)) - const assumptionHyps = unbundleHyps(hyps.filter(hyp => hyp.isAssumption)) - - return <> - {/* {goal.userName &&
case {goal.userName}
} */} - {filter.reverse && goalLi} -
- {! typewriter && objectHyps.length > 0 && -
{t("Objects")}:
- {objectHyps.map((h, i) => )}
} - {!typewriter && assumptionHyps.length > 0 && -
{t("Assumptions")}:
- {assumptionHyps.map((h, i) => )}
} -
- {!filter.reverse && <> -
- - - - -
- {goalLi} - } - {/* {showHints && hints} */} - -}) - -export const MainAssumptions = React.memo((props: GoalProps2) => { - let { t } = useTranslation() - const { goals, filter } = props - - const goal = goals[0] - const filteredList = getFilteredHypotheses(goal.hyps, filter); - const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList; - const locs = React.useContext(LocationsContext) - - const goalLocs = React.useMemo(() => - locs && goal.mvarId ? - { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} : - undefined, - [locs, goal.mvarId]) - - const goalLi =
-
{t("Goal") + ":"}
- - - -
- - const objectHyps = hyps.filter(hyp => !hyp.isAssumption) - const assumptionHyps = hyps.filter(hyp => hyp.isAssumption) - - return
-
{t("Current Goal")}
- {filter.reverse && goalLi} - { objectHyps.length > 0 && -
{t("Objects") + ":"}
- {objectHyps.map((h, i) => )}
} - { assumptionHyps.length > 0 && -
-
{t("Assumptions") + ":"}
- {assumptionHyps.map((h, i) => )} -
} -
-}) - -export const OtherGoals = React.memo((props: GoalProps2) => { - let { t } = useTranslation() - const { goals, filter } = props - return <> - {goals && goals.length > 1 && -
-
{t("Further Goals")}
- {goals.slice(1).map((goal, i) => -
- - - - -
)} -
} - -}) - -interface GoalsProps { - goals: InteractiveGoalsWithHints - filter: GoalFilterState -} - -export function Goals({ goals, filter }: GoalsProps) { - if (goals.goals.length === 0) { - return <> - } else { - return <> - {goals.goals.map((g, i) => )} - - } -} - -interface FilteredGoalsProps { - /** Components to render in the header. */ - headerChildren: React.ReactNode - /** - * When this is `undefined`, the component will not appear at all but will remember its state - * by virtue of still being mounted in the React tree. When it does appear again, the filter - * settings and collapsed state will be as before. */ - goals?: InteractiveGoalsWithHints -} - -/** - * Display goals together with a header containing the provided children as well as buttons - * to control how the goals are displayed. - */ -export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoalsProps) => { - const ec = React.useContext(EditorContext) - - const copyToCommentButton = - { - e.preventDefault(); - if (goals) void ec.copyToComment(goalsWithHintsToString(goals)) - }} - title="copy state to comment" /> - - const [goalFilters, setGoalFilters] = React.useState( - { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }); - - const sortClasses = 'link pointer mh2 dim codicon ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down '); - const sortButton = - setGoalFilters(s => ({ ...s, reverse: !s.reverse }))} /> - - const mkFilterButton = (filterFn: React.SetStateAction, filledFn: (_: GoalFilterState) => boolean, name: string) => - { setGoalFilters(filterFn) }}> -   - {name} - - const filterMenu = - {mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')} -
- {mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')} -
- {mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')} -
- {mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')} - - - const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue - const filterButton = - filterMenu}> - - - - return
-
- - {headerChildren} - {copyToCommentButton}{sortButton}{filterButton} - -
- {goals && } -
-
-
-}) - -export function loadGoals( - rpcSess: RpcSessionAtPos, - uri: string, - setProof: React.Dispatch>, - setCrashed: React.Dispatch>) { -console.info('sending rpc request to load the proof state') - -rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then( - (proof : ProofState) => { - if (typeof proof !== 'undefined') { - console.info(`received a proof state!`) - console.log(proof) - setProof(proof) - setCrashed(false) - } else { - console.warn('received undefined proof state!') - setCrashed(true) - // setProof(undefined) - } - } -).catch((error) => { - setCrashed(true) - console.warn(error) -}) -} - - -export function lastStepHasErrors (proof : ProofState): boolean { - if (!proof?.steps.length) {return false} - - let diags = [...proof.steps[proof.steps.length - 1].diags, ...proof.diagnostics] - - return diags.some( - (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning - ) -} - -export function isLastStepWithErrors (proof : ProofState, i: number): boolean { - if (!proof?.steps.length) {return false} - return (i == proof.steps.length - 1) && lastStepHasErrors(proof) -} +// /** +// * @fileOverview +// * +// * Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx +// */ +// import * as React from 'react' +// // import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api' +// // import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; +// // import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'; +// // import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode' +// // import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips'; +// import { PageContext } from '../../state/context'; +// import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api'; +// // import { RpcSessionAtPos } from '@leanprover/infoview/*'; +// // import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +// import { DiagnosticSeverity } from 'vscode-languageserver-protocol'; +// import { useTranslation } from 'react-i18next'; + +// /** Returns true if `h` is inaccessible according to Lean's default name rendering. */ +// function isInaccessibleName(h: string): boolean { +// return h.indexOf('✝') >= 0; +// } + +// // function goalToString(g: InteractiveGoal): string { +// // let ret = '' + +// // if (g.userName) { +// // ret += `case ${g.userName}\n` +// // } + +// // for (const h of g.hyps) { +// // const names = InteractiveHypothesisBundle_nonAnonymousNames(h).join(' ') +// // ret += `${names} : ${TaggedText_stripTags(h.type)}` +// // if (h.val) { +// // ret += ` := ${TaggedText_stripTags(h.val)}` +// // } +// // ret += '\n' +// // } + +// // ret += `⊢ ${TaggedText_stripTags(g.type)}` + +// // return ret +// // } + +// // export function goalsToString(goals: InteractiveGoals): string { +// // return goals.goals.map(g => goalToString(g)).join('\n\n') +// // } + +// // export function goalsWithHintsToString(goals: InteractiveGoalsWithHints): string { +// // return goals.goals.map(g => goalToString(g.goal)).join('\n\n') +// // } + +// interface GoalFilterState { +// /** If true reverse the list of hypotheses, if false present the order received from LSP. */ +// reverse: boolean, +// /** If true show hypotheses that have isType=True, otherwise hide them. */ +// showType: boolean, +// /** If true show hypotheses that have isInstance=True, otherwise hide them. */ +// showInstance: boolean, +// /** If true show hypotheses that contain a dagger in the name, otherwise hide them. */ +// showHiddenAssumption: boolean +// /** If true show the bodies of let-values, otherwise hide them. */ +// showLetValue: boolean; +// } + +// function getFilteredHypotheses(hyps: InteractiveHypothesisBundle[], filter: GoalFilterState): InteractiveHypothesisBundle[] { +// return hyps.reduce((acc: InteractiveHypothesisBundle[], h) => { +// if (h.isInstance && !filter.showInstance) return acc +// if (h.isType && !filter.showType) return acc +// const names = filter.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n)) +// const hNew: InteractiveHypothesisBundle = filter.showLetValue ? { ...h, names } : { ...h, names, val: undefined } +// if (names.length !== 0) acc.push(hNew) +// return acc +// }, []) +// } + +// interface HypProps { +// hyp: InteractiveHypothesisBundle +// mvarId?: any // MVarId +// } + +// function Hyp({ hyp: h, mvarId }: HypProps) { +// const locs = React.useContext(LocationsContext) + +// const namecls: string = 'mr1 ' + +// (h.isInserted ? 'inserted-text ' : '') + +// (h.isRemoved ? 'removed-text ' : '') + +// const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) => +// +// i ? +// { mvarId, loc: { hyp: h.fvarIds[i] }} : +// undefined +// } +// alwaysHighlight={false} +// >{n} +// ) + +// const typeLocs: Locations | undefined = React.useMemo(() => +// locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ? +// { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds[0], ''] }}} : +// undefined, +// [locs, mvarId, h.fvarIds]) + +// const valLocs: Locations | undefined = React.useMemo(() => +// h.val && locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ? +// { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds[0], ''] }}} : +// undefined, +// [h.val, locs, mvarId, h.fvarIds]) + +// return
+// {names} +// :  +// +// +// +// {h.val && +// +//  :=  +// } +//
+// } + +// interface GoalProps2 { +// goals: InteractiveGoal[] +// filter: GoalFilterState +// } + +// interface GoalProps { +// goal: InteractiveGoal +// filter: GoalFilterState +// showHints?: boolean +// typewriter: boolean +// unbundle?: boolean /** unbundle `x y : Nat` into `x : Nat` and `y : Nat` */ +// } + +// /** +// * Displays the hypotheses, target type and optional case label of a goal according to the +// * provided `filter`. */ +// export const Goal = React.memo((props: GoalProps) => { +// const { goal, filter, showHints, typewriter, unbundle } = props +// let { t } = useTranslation() + +// // TODO: Apparently `goal` can be `undefined` +// if (!goal) {return <>} + +// const filteredList = getFilteredHypotheses(goal.hyps, filter); +// const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList; +// const locs = React.useContext(LocationsContext) +// const goalLocs = React.useMemo(() => +// locs && goal.mvarId ? +// { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} : +// undefined, +// [locs, goal.mvarId]) +// const goalLi =
+// {/*
{t("Goal")}:
*/} +// +// +// +//
+ +// // let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent ' +// // if (props.goal.isInserted) cn += 'b--inserted ' +// // if (props.goal.isRemoved) cn += 'b--removed ' + +// function unbundleHyps (hyps: InteractiveHypothesisBundle[]) : InteractiveHypothesisBundle[] { +// return hyps.flatMap(hyp => ( +// unbundle ? hyp.names.map(name => {return {...hyp, names: [name]}}) : [hyp] +// )) +// } + +// // const hints = +// const objectHyps = unbundleHyps(hyps.filter(hyp => !hyp.isAssumption)) +// const assumptionHyps = unbundleHyps(hyps.filter(hyp => hyp.isAssumption)) + +// return <> +// {/* {goal.userName &&
case {goal.userName}
} */} +// {filter.reverse && goalLi} +//
+// {! typewriter && objectHyps.length > 0 && +//
{t("Objects")}:
+// {objectHyps.map((h, i) => )}
} +// {!typewriter && assumptionHyps.length > 0 && +//
{t("Assumptions")}:
+// {assumptionHyps.map((h, i) => )}
} +//
+// {!filter.reverse && <> +//
+// +// +// +// +//
+// {goalLi} +// } +// {/* {showHints && hints} */} +// +// }) + +// export const MainAssumptions = React.memo((props: GoalProps2) => { +// let { t } = useTranslation() +// const { goals, filter } = props + +// const goal = goals[0] +// const filteredList = getFilteredHypotheses(goal.hyps, filter); +// const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList; +// const locs = React.useContext(LocationsContext) + +// const goalLocs = React.useMemo(() => +// locs && goal.mvarId ? +// { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} : +// undefined, +// [locs, goal.mvarId]) + +// const goalLi =
+//
{t("Goal") + ":"}
+// +// +// +//
+ +// const objectHyps = hyps.filter(hyp => !hyp.isAssumption) +// const assumptionHyps = hyps.filter(hyp => hyp.isAssumption) + +// return
+//
{t("Current Goal")}
+// {filter.reverse && goalLi} +// { objectHyps.length > 0 && +//
{t("Objects") + ":"}
+// {objectHyps.map((h, i) => )}
} +// { assumptionHyps.length > 0 && +//
+//
{t("Assumptions") + ":"}
+// {assumptionHyps.map((h, i) => )} +//
} +//
+// }) + +// export const OtherGoals = React.memo((props: GoalProps2) => { +// let { t } = useTranslation() +// const { goals, filter } = props +// return <> +// {goals && goals.length > 1 && +//
+//
{t("Further Goals")}
+// {goals.slice(1).map((goal, i) => +//
+// +// +// +// +//
)} +//
} +// +// }) + +// interface GoalsProps { +// goals: InteractiveGoalsWithHints +// filter: GoalFilterState +// } + +// export function Goals({ goals, filter }: GoalsProps) { +// if (goals.goals.length === 0) { +// return <> +// } else { +// return <> +// {goals.goals.map((g, i) => )} +// +// } +// } + +// interface FilteredGoalsProps { +// /** Components to render in the header. */ +// headerChildren: React.ReactNode +// /** +// * When this is `undefined`, the component will not appear at all but will remember its state +// * by virtue of still being mounted in the React tree. When it does appear again, the filter +// * settings and collapsed state will be as before. */ +// goals?: InteractiveGoalsWithHints +// } + +// /** +// * Display goals together with a header containing the provided children as well as buttons +// * to control how the goals are displayed. +// */ +// export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoalsProps) => { +// const ec = React.useContext(EditorContext) + +// const copyToCommentButton = +// { +// e.preventDefault(); +// if (goals) void ec.copyToComment(goalsWithHintsToString(goals)) +// }} +// title="copy state to comment" /> + +// const [goalFilters, setGoalFilters] = React.useState( +// { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }); + +// const sortClasses = 'link pointer mh2 dim codicon ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down '); +// const sortButton = +// setGoalFilters(s => ({ ...s, reverse: !s.reverse }))} /> + +// const mkFilterButton = (filterFn: React.SetStateAction, filledFn: (_: GoalFilterState) => boolean, name: string) => +// { setGoalFilters(filterFn) }}> +//   +// {name} +// +// const filterMenu = +// {mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')} +//
+// {mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')} +//
+// {mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')} +//
+// {mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')} +// + +// const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue +// const filterButton = +// filterMenu}> +// +// + +// return
+//
+// +// {headerChildren} +// {copyToCommentButton}{sortButton}{filterButton} +// +//
+// {goals && } +//
+//
+//
+// }) + +// export function loadGoals( +// rpcSess: RpcSessionAtPos, +// uri: string, +// setProof: React.Dispatch>, +// setCrashed: React.Dispatch>) { +// console.info('sending rpc request to load the proof state') + +// rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then( +// (proof : ProofState) => { +// if (typeof proof !== 'undefined') { +// console.info(`received a proof state!`) +// console.log(proof) +// setProof(proof) +// setCrashed(false) +// } else { +// console.warn('received undefined proof state!') +// setCrashed(true) +// // setProof(undefined) +// } +// } +// ).catch((error) => { +// setCrashed(true) +// console.warn(error) +// }) +// } + + +// export function lastStepHasErrors (proof : ProofState): boolean { +// if (!proof?.steps.length) {return false} + +// let diags = [...proof.steps[proof.steps.length - 1].diags, ...proof.diagnostics] + +// return diags.some( +// (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning +// ) +// } + +// export function isLastStepWithErrors (proof : ProofState, i: number): boolean { +// if (!proof?.steps.length) {return false} +// return (i == proof.steps.length - 1) && lastStepHasErrors(proof) +// } diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx index d77ae8a..da67148 100644 --- a/client/src/components/infoview/info.tsx +++ b/client/src/components/infoview/info.tsx @@ -1,442 +1,442 @@ -/* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/info.tsx */ - -import * as React from 'react' -import { CircularProgress } from '@mui/material' -import type { Location, Diagnostic } from 'vscode-languageserver-protocol' -import { getInteractiveTermGoal, InteractiveDiagnostic, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError, - RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api' -import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound, - mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util' -import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts' -import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/infoview/userWidget' -import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions' -import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation' - -import { AllMessages, lspDiagToInteractive } from './messages' -import { goalsToString, Goal, MainAssumptions, OtherGoals } from './goals' -import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api' -import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from '../../state/context' -import { useTranslation } from 'react-i18next' -import { GoalsTabs } from './main' - -// TODO: All about pinning could probably be removed -type InfoKind = 'cursor' | 'pin' - -interface InfoPinnable { - kind: InfoKind - /** Takes an argument for caching reasons, but should only ever (un)pin itself. */ - onPin: (pos: DocumentPosition) => void -} - -interface InfoStatusBarProps extends InfoPinnable, PausableProps { - pos: DocumentPosition - status: InfoStatus - triggerUpdate: () => Promise -} - -const InfoStatusBar = React.memo((props: InfoStatusBarProps) => { - const { kind, onPin, status, pos, isPaused, setPaused, triggerUpdate } = props - - const ec = React.useContext(EditorContext) - - const statusColTable: {[T in InfoStatus]: string} = { - 'updating': 'gold ', - 'error': 'dark-red ', - 'ready': '', - } - const statusColor = statusColTable[status] - const locationString = `${basename(pos.uri)}:${pos.line+1}:${pos.character}` - const isPinned = kind === 'pin' - - return ( - - {locationString} - {isPinned && !isPaused && ' (pinned)'} - {!isPinned && isPaused && ' (paused)'} - {isPinned && isPaused && ' (pinned and paused)'} - - {isPinned && - { e.preventDefault(); void ec.revealPosition(pos); }} - title='reveal file location' />} - { e.preventDefault(); onPin(pos); }} - title={isPinned ? 'unpin' : 'pin'} /> - { e.preventDefault(); setPaused(!isPaused) }} - title={isPaused ? 'continue updating' : 'pause updating'} /> - { e.preventDefault(); void triggerUpdate() }} - title='update'/> - - - ) -}) - -interface InfoDisplayContentProps extends PausableProps { - pos: DocumentPosition - messages: InteractiveDiagnostic[] - goals?: InteractiveGoals - termGoal?: InteractiveTermGoal - error?: string - userWidgets: UserWidgetInstance[] - triggerUpdate: () => Promise - proofString? : string -} - -const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { - let { t } = useTranslation() - const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props - - const hasWidget = userWidgets.length > 0 - const hasError = !!error - const hasMessages = messages.length !== 0 - - const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget - - const [selectedLocs, setSelectedLocs] = React.useState([]) - React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character]) - - const locs: Locations = React.useMemo(() => ({ - isSelected: (l: GoalsLocation) => selectedLocs.some(v => GoalsLocation.isEqual(v, l)), - setSelected: (l, act) => setSelectedLocs(ls => { - // We ensure that `selectedLocs` maintains its reference identity if the selection - // status of `l` didn't change. - const newLocs = ls.filter(v => !GoalsLocation.isEqual(v, l)) - const wasSelected = newLocs.length !== ls.length - const isSelected = typeof act === 'function' ? act(wasSelected) : act - if (isSelected) newLocs.push(l) - return wasSelected === isSelected ? ls : newLocs - }), - subexprTemplate: undefined - }), [selectedLocs]) - - const goalFilter = { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true } - /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */ - - return <> - {hasError && - } - {/* TODO: Move error messages to Chat instead */} - -
- - { goals && goals.goals.length > 0 && <> - ({goal: goal, hints: []}))} last={false} onClick={() => {}} onGoalChange={() => {}}/> - {/* - */} - } -
- {/*
- { goals && (goals.goals.length > 0 - ? - :
{t("No Goals")}
- )} -
*/} - - {/* {userWidgets.map(widget => -
- {widget.name} - -
- )} */} - {/* {nothingToShow && ( - isPaused ? - /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 * / - Updating is paused.{' '} - { e.preventDefault(); void triggerUpdate() }}>Refresh - {' '}or { e.preventDefault(); setPaused(false) }}>resume updating - {' '}to see information. - : - <>
{t("Loading goal…")}
)} */} - {/* - {goals && goals.goals.length > 1 &&
-
Weitere Goals
- - {goals.goals.slice(1).map((goal, i) => -
)} -
} - */} - -}) - -interface InfoDisplayProps { - pos: DocumentPosition, - status: InfoStatus, - messages: InteractiveDiagnostic[], - proof?: ProofState, - goals?: InteractiveGoals, - termGoal?: InteractiveTermGoal, - error?: string, - userWidgets: UserWidgetInstance[], - rpcSess: RpcSessionAtPos, - triggerUpdate: () => Promise, -} - -/** Displays goal state and messages. Can be paused. */ -function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) { - // Used to update the paused state *just once* if it is paused, - // but a display update is triggered - const [shouldRefresh, setShouldRefresh] = React.useState(false) - const [{ isPaused, setPaused }, props, propsRef] = usePausableState(false, props0) - if (shouldRefresh) { - propsRef.current = props0 - setShouldRefresh(false) - } - const triggerDisplayUpdate = async () => { - await props0.triggerUpdate() - setShouldRefresh(true) - } - - const {kind, goals, rpcSess} = props - - const ec = React.useContext(EditorContext) - - // If we are the cursor infoview, then we should subscribe to - // some commands from the editor extension - const isCursor = kind === 'cursor' - useEvent(ec.events.requestedAction, act => { - if (!isCursor) return - if (act.kind !== 'copyToComment') return - if (goals) void ec.copyToComment(goalsToString(goals)) - }, [goals]) - useEvent(ec.events.requestedAction, act => { - if (!isCursor) return - if (act.kind !== 'togglePaused') return - setPaused(isPaused => !isPaused) - }) - - const editor = React.useContext(MonacoEditorContext) - - return ( - - {/*
*/} - {/* */} -
- -
- {/*
*/} - - ) -} - -/** - * Note: in the cursor view, we have to keep the cursor position as part of the component state - * to avoid flickering when the cursor moved. Otherwise, the component is re-initialised and the - * goal states reset to `undefined` on cursor moves. - */ -export type InfoProps = InfoPinnable & { pos?: DocumentPosition } - -/** Fetches info from the server and renders an {@link InfoDisplay}. */ -export function Info(props: InfoProps) { - if (props.kind === 'cursor') return - else return -} - -function InfoAtCursor(props: InfoProps) { - const ec = React.useContext(EditorContext) - // eslint-disable-next-line @typescript-eslint/no-non-null-assertion - const [curLoc, setCurLoc] = React.useState(ec.events.changedCursorLocation.current!) - useEvent(ec.events.changedCursorLocation, loc => loc && setCurLoc(loc), []) - const pos = { uri: curLoc.uri, ...curLoc.range.start } - return -} - -function useIsProcessingAt(p: DocumentPosition): boolean { - const allProgress = React.useContext(ProgressContext) - const processing = allProgress.get(p.uri) - if (!processing) return false - return processing.some(i => RangeHelpers.contains(i.range, p)) -} - -function InfoAux(props: InfoProps) { - - const { setProof } = React.useContext(ProofContext) - - const config = React.useContext(ConfigContext) - - // eslint-disable-next-line @typescript-eslint/no-non-null-assertion - const pos = props.pos! - const rpcSess = useRpcSessionAtPos(pos) - - // Compute the LSP diagnostics at this info's position. We try to ensure that if these remain - // the same, then so does the identity of `lspDiagsHere` so that it can be used as a dep. - const lspDiags = React.useContext(LspDiagnosticsContext) - const [lspDiagsHere, setLspDiagsHere] = React.useState([]) - React.useEffect(() => { - // Note: the curly braces are important. https://medium.com/geekculture/react-uncaught-typeerror-destroy-is-not-a-function-192738a6e79b - setLspDiagsHere(diags0 => { - const diagPred = (d: Diagnostic) => - RangeHelpers.contains(d.range, pos, config.allErrorsOnLine) - const newDiags = (lspDiags.get(pos.uri) || []).filter(diagPred) - if (newDiags.length === diags0.length && newDiags.every((d, i) => d === diags0[i])) return diags0 - return newDiags - }) - }, [lspDiags, pos.uri, pos.line, pos.character, config.allErrorsOnLine]) - - const serverIsProcessing = useIsProcessingAt(pos) - - // This is a virtual dep of the info-requesting function. It is bumped whenever the Lean server - // indicates that another request should be made. Bumping it dirties the dep state of - // `useAsyncWithTrigger` below, causing the `useEffect` lower down in this component to - // make the request. We cannot simply call `triggerUpdateCore` because `useAsyncWithTrigger` - // does not support reentrancy like that. - const [updaterTick, setUpdaterTick] = React.useState(0) - - // For atomicity, we use a single update function that fetches all the info at `pos` at once. - // Besides what the server replies with, we also include the inputs (deps) in this type so - // that the displayed state cannot ever get out of sync by showing an old reply together - // with e.g. a new `pos`. - type InfoRequestResult = Omit - const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise((resolve, reject) => { - - const proofReq = rpcSess.call('Game.getProofState', DocumentPosition.toTdpp(pos)).catch((error) => { - console.warn(error) - }) - const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos)) - const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos)) - const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound) - const messagesReq = getInteractiveDiagnostics(rpcSess, {start: pos.line, end: pos.line+1}) - // fall back to non-interactive diagnostics when lake fails - // (see https://github.com/leanprover/vscode-lean4/issues/90) - .then(diags => diags.length === 0 ? lspDiagsHere.map(lspDiagToInteractive) : diags) - - // While `lake print-paths` is running, the output of Lake is shown as - // info diagnostics on line 1. However, all RPC requests block until - // Lake is finished, so we don't see these diagnostics while Lake is - // building. Therefore we show the LSP diagnostics on line 1 if the - // server does not respond within half a second. - if (pos.line === 0 && lspDiagsHere.length) { - setTimeout(() => resolve({ - pos, - status: 'updating', - messages: lspDiagsHere.map(lspDiagToInteractive), - proof: undefined, - goals: undefined, - termGoal: undefined, - error: undefined, - userWidgets: [], - rpcSess - }), 500) - } - - // NB: it is important to await await reqs at once, otherwise - // if both throw then one exception becomes unhandled. - Promise.all([proofReq, goalsReq, termGoalReq, widgetsReq, messagesReq]).then( - ([proof, goals, termGoal, userWidgets, messages]) => resolve({ - pos, - status: 'ready', - messages, - proof : proof as any, - goals: goals as any, - termGoal, - error: undefined, - userWidgets: userWidgets?.widgets ?? [], - rpcSess - }), - ex => { - if (ex?.code === RpcErrorCode.ContentModified || - ex?.code === RpcErrorCode.RpcNeedsReconnect) { - // Document has been changed since we made the request, or we need to reconnect - // to the RPC sessions. Try again. - setUpdaterTick(t => t + 1) - reject('retry') - } - - let errorString = '' - if (typeof ex === 'string') { - errorString = ex - } else if (isRpcError(ex)) { - errorString = mapRpcError(ex).message - } else if (ex instanceof Error) { - errorString = ex.toString() - } else { - errorString = `Unrecognized error: ${JSON.stringify(ex)}` - } - - resolve({ - pos, - status: 'error', - messages: lspDiagsHere.map(lspDiagToInteractive), - proof: undefined, - goals: undefined, - termGoal: undefined, - error: `Error fetching goals: ${errorString}`, - userWidgets: [], - rpcSess - }) - } - ) - }), [updaterTick, pos.uri, pos.line, pos.character, rpcSess, serverIsProcessing, lspDiagsHere]) - - // We use a timeout to debounce info requests. Whenever a request is already scheduled - // but something happens that warrants a request for newer info, we cancel the old request - // and schedule just the new one. - const updaterTimeout = React.useRef() - const clearUpdaterTimeout = () => { - if (updaterTimeout.current) { - window.clearTimeout(updaterTimeout.current) - updaterTimeout.current = undefined - } - } - const triggerUpdate = React.useCallback(() => new Promise(resolve => { - clearUpdaterTimeout() - const tm = window.setTimeout(() => { - void triggerUpdateCore().then(resolve) - updaterTimeout.current = undefined - }, config.debounceTime) - // Hack: even if the request is cancelled, the promise should resolve so that no `await` - // is left waiting forever. We ensure this happens in a simple way. - window.setTimeout(resolve, config.debounceTime) - updaterTimeout.current = tm - }), [triggerUpdateCore, config.debounceTime]) - - const [displayProps, setDisplayProps] = React.useState({ - pos, - status: 'updating', - messages: [], - proof: undefined, - goals: undefined, - termGoal: undefined, - error: undefined, - userWidgets: [], - rpcSess, - triggerUpdate - }) - - // Propagates changes in the state of async info requests to the display props, - // and re-requests info if needed. - // This effect triggers new requests for info whenever need. It also propagates changes - // in the state of the `useAsyncWithTrigger` to the displayed props. - React.useEffect(() => { - if (state.state === 'notStarted') - void triggerUpdate() - else if (state.state === 'loading') { - setDisplayProps(dp => ({ ...dp, status: 'updating' })) - } - else if (state.state === 'resolved') { - // if (state.value.goals?.goals?.length) { - // hintContext.setHints(state.value.goals.goals[0].hints) - // } - setDisplayProps({ ...state.value, triggerUpdate }) - - // Update the game's proof state - console.info('updating proof from editor mode.') - setProof(state.value.proof) - - } else if (state.state === 'rejected' && state.error !== 'retry') { - // The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception. - console.warn('Unreachable code reached with error: ', state.error) - } - }, [state]) - - return -} +// /* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/info.tsx */ + +// import * as React from 'react' +// import { CircularProgress } from '@mui/material' +// import type { Location, Diagnostic } from 'vscode-languageserver-protocol' +// import { getInteractiveTermGoal, InteractiveDiagnostic, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError, +// RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api' +// import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound, +// mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util' +// import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts' +// import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/infoview/userWidget' +// import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions' +// import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation' + +// import { AllMessages, lspDiagToInteractive } from './messages' +// // import { goalsToString, Goal, MainAssumptions, OtherGoals } from './goals' +// import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api' +// import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from '../../state/context' +// import { useTranslation } from 'react-i18next' +// import { GoalsTabs } from './main' + +// // TODO: All about pinning could probably be removed +// type InfoKind = 'cursor' | 'pin' + +// interface InfoPinnable { +// kind: InfoKind +// /** Takes an argument for caching reasons, but should only ever (un)pin itself. */ +// onPin: (pos: DocumentPosition) => void +// } + +// interface InfoStatusBarProps extends InfoPinnable, PausableProps { +// pos: DocumentPosition +// status: InfoStatus +// triggerUpdate: () => Promise +// } + +// const InfoStatusBar = React.memo((props: InfoStatusBarProps) => { +// const { kind, onPin, status, pos, isPaused, setPaused, triggerUpdate } = props + +// const ec = React.useContext(EditorContext) + +// const statusColTable: {[T in InfoStatus]: string} = { +// 'updating': 'gold ', +// 'error': 'dark-red ', +// 'ready': '', +// } +// const statusColor = statusColTable[status] +// const locationString = `${basename(pos.uri)}:${pos.line+1}:${pos.character}` +// const isPinned = kind === 'pin' + +// return ( +// +// {locationString} +// {isPinned && !isPaused && ' (pinned)'} +// {!isPinned && isPaused && ' (paused)'} +// {isPinned && isPaused && ' (pinned and paused)'} +// +// {isPinned && +// { e.preventDefault(); void ec.revealPosition(pos); }} +// title='reveal file location' />} +// { e.preventDefault(); onPin(pos); }} +// title={isPinned ? 'unpin' : 'pin'} /> +// { e.preventDefault(); setPaused(!isPaused) }} +// title={isPaused ? 'continue updating' : 'pause updating'} /> +// { e.preventDefault(); void triggerUpdate() }} +// title='update'/> +// +// +// ) +// }) + +// interface InfoDisplayContentProps extends PausableProps { +// pos: DocumentPosition +// messages: InteractiveDiagnostic[] +// goals?: InteractiveGoals +// termGoal?: InteractiveTermGoal +// error?: string +// userWidgets: UserWidgetInstance[] +// triggerUpdate: () => Promise +// proofString? : string +// } + +// const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { +// let { t } = useTranslation() +// const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props + +// const hasWidget = userWidgets.length > 0 +// const hasError = !!error +// const hasMessages = messages.length !== 0 + +// const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget + +// const [selectedLocs, setSelectedLocs] = React.useState([]) +// React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character]) + +// const locs: Locations = React.useMemo(() => ({ +// isSelected: (l: GoalsLocation) => selectedLocs.some(v => GoalsLocation.isEqual(v, l)), +// setSelected: (l, act) => setSelectedLocs(ls => { +// // We ensure that `selectedLocs` maintains its reference identity if the selection +// // status of `l` didn't change. +// const newLocs = ls.filter(v => !GoalsLocation.isEqual(v, l)) +// const wasSelected = newLocs.length !== ls.length +// const isSelected = typeof act === 'function' ? act(wasSelected) : act +// if (isSelected) newLocs.push(l) +// return wasSelected === isSelected ? ls : newLocs +// }), +// subexprTemplate: undefined +// }), [selectedLocs]) + +// const goalFilter = { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true } +// /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */ + +// return <> +// {hasError && +// } +// {/* TODO: Move error messages to Chat instead */} +// +//
+ +// { goals && goals.goals.length > 0 && <> +// ({goal: goal, hints: []}))} last={false} onClick={() => {}} onGoalChange={() => {}}/> +// {/* +// */} +// } +//
+// {/*
+// { goals && (goals.goals.length > 0 +// ? +// :
{t("No Goals")}
+// )} +//
*/} +// +// {/* {userWidgets.map(widget => +//
+// {widget.name} +// +//
+// )} */} +// {/* {nothingToShow && ( +// isPaused ? +// /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 * / +// Updating is paused.{' '} +// { e.preventDefault(); void triggerUpdate() }}>Refresh +// {' '}or { e.preventDefault(); setPaused(false) }}>resume updating +// {' '}to see information. +// : +// <>
{t("Loading goal…")}
)} */} +// {/* +// {goals && goals.goals.length > 1 &&
+//
Weitere Goals
+ +// {goals.goals.slice(1).map((goal, i) => +//
)} +//
} +// */} +// +// }) + +// interface InfoDisplayProps { +// pos: DocumentPosition, +// status: InfoStatus, +// messages: InteractiveDiagnostic[], +// proof?: ProofState, +// goals?: InteractiveGoals, +// termGoal?: InteractiveTermGoal, +// error?: string, +// userWidgets: UserWidgetInstance[], +// rpcSess: RpcSessionAtPos, +// triggerUpdate: () => Promise, +// } + +// /** Displays goal state and messages. Can be paused. */ +// function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) { +// // Used to update the paused state *just once* if it is paused, +// // but a display update is triggered +// const [shouldRefresh, setShouldRefresh] = React.useState(false) +// const [{ isPaused, setPaused }, props, propsRef] = usePausableState(false, props0) +// if (shouldRefresh) { +// propsRef.current = props0 +// setShouldRefresh(false) +// } +// const triggerDisplayUpdate = async () => { +// await props0.triggerUpdate() +// setShouldRefresh(true) +// } + +// const {kind, goals, rpcSess} = props + +// const ec = React.useContext(EditorContext) + +// // If we are the cursor infoview, then we should subscribe to +// // some commands from the editor extension +// const isCursor = kind === 'cursor' +// useEvent(ec.events.requestedAction, act => { +// if (!isCursor) return +// if (act.kind !== 'copyToComment') return +// if (goals) void ec.copyToComment(goalsToString(goals)) +// }, [goals]) +// useEvent(ec.events.requestedAction, act => { +// if (!isCursor) return +// if (act.kind !== 'togglePaused') return +// setPaused(isPaused => !isPaused) +// }) + +// const editor = React.useContext(MonacoEditorContext) + +// return ( +// +// {/*
*/} +// {/* */} +//
+// +//
+// {/*
*/} +// +// ) +// } + +// /** +// * Note: in the cursor view, we have to keep the cursor position as part of the component state +// * to avoid flickering when the cursor moved. Otherwise, the component is re-initialised and the +// * goal states reset to `undefined` on cursor moves. +// */ +// export type InfoProps = InfoPinnable & { pos?: DocumentPosition } + +// /** Fetches info from the server and renders an {@link InfoDisplay}. */ +// export function Info(props: InfoProps) { +// if (props.kind === 'cursor') return +// else return +// } + +// function InfoAtCursor(props: InfoProps) { +// const ec = React.useContext(EditorContext) +// // eslint-disable-next-line @typescript-eslint/no-non-null-assertion +// const [curLoc, setCurLoc] = React.useState(ec.events.changedCursorLocation.current!) +// useEvent(ec.events.changedCursorLocation, loc => loc && setCurLoc(loc), []) +// const pos = { uri: curLoc.uri, ...curLoc.range.start } +// return +// } + +// function useIsProcessingAt(p: DocumentPosition): boolean { +// const allProgress = React.useContext(ProgressContext) +// const processing = allProgress.get(p.uri) +// if (!processing) return false +// return processing.some(i => RangeHelpers.contains(i.range, p)) +// } + +// function InfoAux(props: InfoProps) { + +// const { setProof } = React.useContext(ProofContext) + +// const config = React.useContext(ConfigContext) + +// // eslint-disable-next-line @typescript-eslint/no-non-null-assertion +// const pos = props.pos! +// const rpcSess = useRpcSessionAtPos(pos) + +// // Compute the LSP diagnostics at this info's position. We try to ensure that if these remain +// // the same, then so does the identity of `lspDiagsHere` so that it can be used as a dep. +// const lspDiags = React.useContext(LspDiagnosticsContext) +// const [lspDiagsHere, setLspDiagsHere] = React.useState([]) +// React.useEffect(() => { +// // Note: the curly braces are important. https://medium.com/geekculture/react-uncaught-typeerror-destroy-is-not-a-function-192738a6e79b +// setLspDiagsHere(diags0 => { +// const diagPred = (d: Diagnostic) => +// RangeHelpers.contains(d.range, pos, config.allErrorsOnLine) +// const newDiags = (lspDiags.get(pos.uri) || []).filter(diagPred) +// if (newDiags.length === diags0.length && newDiags.every((d, i) => d === diags0[i])) return diags0 +// return newDiags +// }) +// }, [lspDiags, pos.uri, pos.line, pos.character, config.allErrorsOnLine]) + +// const serverIsProcessing = useIsProcessingAt(pos) + +// // This is a virtual dep of the info-requesting function. It is bumped whenever the Lean server +// // indicates that another request should be made. Bumping it dirties the dep state of +// // `useAsyncWithTrigger` below, causing the `useEffect` lower down in this component to +// // make the request. We cannot simply call `triggerUpdateCore` because `useAsyncWithTrigger` +// // does not support reentrancy like that. +// const [updaterTick, setUpdaterTick] = React.useState(0) + +// // For atomicity, we use a single update function that fetches all the info at `pos` at once. +// // Besides what the server replies with, we also include the inputs (deps) in this type so +// // that the displayed state cannot ever get out of sync by showing an old reply together +// // with e.g. a new `pos`. +// type InfoRequestResult = Omit +// const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise((resolve, reject) => { + +// const proofReq = rpcSess.call('Game.getProofState', DocumentPosition.toTdpp(pos)).catch((error) => { +// console.warn(error) +// }) +// const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos)) +// const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos)) +// const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound) +// const messagesReq = getInteractiveDiagnostics(rpcSess, {start: pos.line, end: pos.line+1}) +// // fall back to non-interactive diagnostics when lake fails +// // (see https://github.com/leanprover/vscode-lean4/issues/90) +// .then(diags => diags.length === 0 ? lspDiagsHere.map(lspDiagToInteractive) : diags) + +// // While `lake print-paths` is running, the output of Lake is shown as +// // info diagnostics on line 1. However, all RPC requests block until +// // Lake is finished, so we don't see these diagnostics while Lake is +// // building. Therefore we show the LSP diagnostics on line 1 if the +// // server does not respond within half a second. +// if (pos.line === 0 && lspDiagsHere.length) { +// setTimeout(() => resolve({ +// pos, +// status: 'updating', +// messages: lspDiagsHere.map(lspDiagToInteractive), +// proof: undefined, +// goals: undefined, +// termGoal: undefined, +// error: undefined, +// userWidgets: [], +// rpcSess +// }), 500) +// } + +// // NB: it is important to await await reqs at once, otherwise +// // if both throw then one exception becomes unhandled. +// Promise.all([proofReq, goalsReq, termGoalReq, widgetsReq, messagesReq]).then( +// ([proof, goals, termGoal, userWidgets, messages]) => resolve({ +// pos, +// status: 'ready', +// messages, +// proof : proof as any, +// goals: goals as any, +// termGoal, +// error: undefined, +// userWidgets: userWidgets?.widgets ?? [], +// rpcSess +// }), +// ex => { +// if (ex?.code === RpcErrorCode.ContentModified || +// ex?.code === RpcErrorCode.RpcNeedsReconnect) { +// // Document has been changed since we made the request, or we need to reconnect +// // to the RPC sessions. Try again. +// setUpdaterTick(t => t + 1) +// reject('retry') +// } + +// let errorString = '' +// if (typeof ex === 'string') { +// errorString = ex +// } else if (isRpcError(ex)) { +// errorString = mapRpcError(ex).message +// } else if (ex instanceof Error) { +// errorString = ex.toString() +// } else { +// errorString = `Unrecognized error: ${JSON.stringify(ex)}` +// } + +// resolve({ +// pos, +// status: 'error', +// messages: lspDiagsHere.map(lspDiagToInteractive), +// proof: undefined, +// goals: undefined, +// termGoal: undefined, +// error: `Error fetching goals: ${errorString}`, +// userWidgets: [], +// rpcSess +// }) +// } +// ) +// }), [updaterTick, pos.uri, pos.line, pos.character, rpcSess, serverIsProcessing, lspDiagsHere]) + +// // We use a timeout to debounce info requests. Whenever a request is already scheduled +// // but something happens that warrants a request for newer info, we cancel the old request +// // and schedule just the new one. +// const updaterTimeout = React.useRef() +// const clearUpdaterTimeout = () => { +// if (updaterTimeout.current) { +// window.clearTimeout(updaterTimeout.current) +// updaterTimeout.current = undefined +// } +// } +// const triggerUpdate = React.useCallback(() => new Promise(resolve => { +// clearUpdaterTimeout() +// const tm = window.setTimeout(() => { +// void triggerUpdateCore().then(resolve) +// updaterTimeout.current = undefined +// }, config.debounceTime) +// // Hack: even if the request is cancelled, the promise should resolve so that no `await` +// // is left waiting forever. We ensure this happens in a simple way. +// window.setTimeout(resolve, config.debounceTime) +// updaterTimeout.current = tm +// }), [triggerUpdateCore, config.debounceTime]) + +// const [displayProps, setDisplayProps] = React.useState({ +// pos, +// status: 'updating', +// messages: [], +// proof: undefined, +// goals: undefined, +// termGoal: undefined, +// error: undefined, +// userWidgets: [], +// rpcSess, +// triggerUpdate +// }) + +// // Propagates changes in the state of async info requests to the display props, +// // and re-requests info if needed. +// // This effect triggers new requests for info whenever need. It also propagates changes +// // in the state of the `useAsyncWithTrigger` to the displayed props. +// React.useEffect(() => { +// if (state.state === 'notStarted') +// void triggerUpdate() +// else if (state.state === 'loading') { +// setDisplayProps(dp => ({ ...dp, status: 'updating' })) +// } +// else if (state.state === 'resolved') { +// // if (state.value.goals?.goals?.length) { +// // hintContext.setHints(state.value.goals.goals[0].hints) +// // } +// setDisplayProps({ ...state.value, triggerUpdate }) + +// // Update the game's proof state +// console.info('updating proof from editor mode.') +// setProof(state.value.proof) + +// } else if (state.state === 'rejected' && state.error !== 'retry') { +// // The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception. +// console.warn('Unreachable code reached with error: ', state.error) +// } +// }, [state]) + +// return +// } diff --git a/client/src/components/infoview/infos.tsx b/client/src/components/infoview/infos.tsx index bf41a68..3ca5e9b 100644 --- a/client/src/components/infoview/infos.tsx +++ b/client/src/components/infoview/infos.tsx @@ -1,133 +1,133 @@ -/* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/infos.tsx */ - -import * as React from 'react'; -import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, TextDocumentContentChangeEvent } from 'vscode-languageserver-protocol'; - -import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; -import { DocumentPosition, Keyed, PositionHelpers, useClientNotificationEffect, useClientNotificationState, useEvent, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util'; -import { Info, InfoProps } from './info'; -import { useTranslation } from 'react-i18next'; - -/** Manages and displays pinned infos, as well as info for the current location. */ -export function Infos() { - let { t } = useTranslation() - const ec = React.useContext(EditorContext); - - // Update pins when the document changes. In particular, when edits are made - // earlier in the text such that a pin has to move up or down. - const [pinnedPositions, setPinnedPositions] = useClientNotificationState( - 'textDocument/didChange', - new Array>(), - (pinnedPositions, params: DidChangeTextDocumentParams) => { - if (pinnedPositions.length === 0) return pinnedPositions; - - let changed: boolean = false; - const newPins = pinnedPositions.map(pin => { - if (pin.uri !== params.textDocument.uri) return pin; - // NOTE(WN): It's important to make a clone here, otherwise this - // actually mutates the pin. React state updates must be pure. - // See https://github.com/facebook/react/issues/12856 - const newPin: Keyed = { ...pin }; - for (const chg of params.contentChanges) { - if (!TextDocumentContentChangeEvent.isIncremental(chg)) { - changed = true; - return null; - } - if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.start)) continue; - // We can assume chg.range.start < pin - - // If the pinned position is replaced with new text, just delete the pin. - if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.end)) { - changed = true; - return null; - } - - const oldPin = { ...newPin }; - - // How many lines before the pin position were added by the change. - // Can be negative when more lines are removed than added. - let additionalLines = 0; - let lastLineLen = chg.range.start.character; - for (const c of chg.text) - if (c === '\n') { - additionalLines++; - lastLineLen = 0; - } else lastLineLen++; - - // Subtract lines that were already present - additionalLines -= (chg.range.end.line - chg.range.start.line) - newPin.line += additionalLines; - - if (oldPin.line < chg.range.end.line) { - // Should never execute by the <= check above. - throw new Error('unreachable code reached') - } else if (oldPin.line === chg.range.end.line) { - newPin.character = lastLineLen + (oldPin.character - chg.range.end.character); - } - } - if (!DocumentPosition.isEqual(newPin, pin)) changed = true; - - // NOTE(WN): We maintain the `key` when a pin is moved around to maintain - // its component identity and minimise flickering. - return newPin; - }); - - if (changed) return newPins.filter(p => p !== null) as Keyed[]; - return pinnedPositions; - }, - [] - ); - - // Remove pins for closed documents - useClientNotificationEffect( - 'textDocument/didClose', - (params: DidCloseTextDocumentParams) => { - setPinnedPositions(pinnedPositions => pinnedPositions.filter(p => p.uri !== params.textDocument.uri)); - }, - [] - ); - - const curPos: DocumentPosition | undefined = - useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) - - // Update pins on UI actions - const pinKey = React.useRef(0); - const isPinned = (pinnedPositions: DocumentPosition[], pos: DocumentPosition) => { - return pinnedPositions.some(p => DocumentPosition.isEqual(p, pos)); - } - const pin = React.useCallback((pos: DocumentPosition) => { - setPinnedPositions(pinnedPositions => { - if (isPinned(pinnedPositions, pos)) return pinnedPositions; - pinKey.current += 1; - return [ ...pinnedPositions, { ...pos, key: pinKey.current.toString() } ]; - }); - }, []); - const unpin = React.useCallback((pos: DocumentPosition) => { - setPinnedPositions(pinnedPositions => { - if (!isPinned(pinnedPositions, pos)) return pinnedPositions; - return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, pos)); - }); - }, []); - - // Toggle pin at current position when the editor requests it - useEvent(ec.events.requestedAction, act => { - if (act.kind !== 'togglePin') return - if (!curPos) return - setPinnedPositions(pinnedPositions => { - if (isPinned(pinnedPositions, curPos)) { - return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, curPos)); - } else { - pinKey.current += 1; - return [ ...pinnedPositions, { ...curPos, key: pinKey.current.toString() } ]; - } - }); - }, [curPos?.uri, curPos?.line, curPos?.character]); - - const infoProps: Keyed[] = pinnedPositions.map(pos => ({ kind: 'pin', onPin: unpin, pos, key: pos.key })); - if (curPos) infoProps.push({ kind: 'cursor', onPin: pin, key: 'cursor' }); - - return
- {infoProps.map (ps => )} - {!curPos &&

{t("Click somewhere in the Lean file to enable the infoview.")}

} -
; -} +// /* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/infos.tsx */ + +// import * as React from 'react'; +// import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, TextDocumentContentChangeEvent } from 'vscode-languageserver-protocol'; + +// import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; +// import { DocumentPosition, Keyed, PositionHelpers, useClientNotificationEffect, useClientNotificationState, useEvent, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +// import { Info, InfoProps } from './info'; +// import { useTranslation } from 'react-i18next'; + +// /** Manages and displays pinned infos, as well as info for the current location. */ +// export function Infos() { +// let { t } = useTranslation() +// const ec = React.useContext(EditorContext); + +// // Update pins when the document changes. In particular, when edits are made +// // earlier in the text such that a pin has to move up or down. +// const [pinnedPositions, setPinnedPositions] = useClientNotificationState( +// 'textDocument/didChange', +// new Array>(), +// (pinnedPositions, params: DidChangeTextDocumentParams) => { +// if (pinnedPositions.length === 0) return pinnedPositions; + +// let changed: boolean = false; +// const newPins = pinnedPositions.map(pin => { +// if (pin.uri !== params.textDocument.uri) return pin; +// // NOTE(WN): It's important to make a clone here, otherwise this +// // actually mutates the pin. React state updates must be pure. +// // See https://github.com/facebook/react/issues/12856 +// const newPin: Keyed = { ...pin }; +// for (const chg of params.contentChanges) { +// if (!TextDocumentContentChangeEvent.isIncremental(chg)) { +// changed = true; +// return null; +// } +// if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.start)) continue; +// // We can assume chg.range.start < pin + +// // If the pinned position is replaced with new text, just delete the pin. +// if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.end)) { +// changed = true; +// return null; +// } + +// const oldPin = { ...newPin }; + +// // How many lines before the pin position were added by the change. +// // Can be negative when more lines are removed than added. +// let additionalLines = 0; +// let lastLineLen = chg.range.start.character; +// for (const c of chg.text) +// if (c === '\n') { +// additionalLines++; +// lastLineLen = 0; +// } else lastLineLen++; + +// // Subtract lines that were already present +// additionalLines -= (chg.range.end.line - chg.range.start.line) +// newPin.line += additionalLines; + +// if (oldPin.line < chg.range.end.line) { +// // Should never execute by the <= check above. +// throw new Error('unreachable code reached') +// } else if (oldPin.line === chg.range.end.line) { +// newPin.character = lastLineLen + (oldPin.character - chg.range.end.character); +// } +// } +// if (!DocumentPosition.isEqual(newPin, pin)) changed = true; + +// // NOTE(WN): We maintain the `key` when a pin is moved around to maintain +// // its component identity and minimise flickering. +// return newPin; +// }); + +// if (changed) return newPins.filter(p => p !== null) as Keyed[]; +// return pinnedPositions; +// }, +// [] +// ); + +// // Remove pins for closed documents +// useClientNotificationEffect( +// 'textDocument/didClose', +// (params: DidCloseTextDocumentParams) => { +// setPinnedPositions(pinnedPositions => pinnedPositions.filter(p => p.uri !== params.textDocument.uri)); +// }, +// [] +// ); + +// const curPos: DocumentPosition | undefined = +// useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) + +// // Update pins on UI actions +// const pinKey = React.useRef(0); +// const isPinned = (pinnedPositions: DocumentPosition[], pos: DocumentPosition) => { +// return pinnedPositions.some(p => DocumentPosition.isEqual(p, pos)); +// } +// const pin = React.useCallback((pos: DocumentPosition) => { +// setPinnedPositions(pinnedPositions => { +// if (isPinned(pinnedPositions, pos)) return pinnedPositions; +// pinKey.current += 1; +// return [ ...pinnedPositions, { ...pos, key: pinKey.current.toString() } ]; +// }); +// }, []); +// const unpin = React.useCallback((pos: DocumentPosition) => { +// setPinnedPositions(pinnedPositions => { +// if (!isPinned(pinnedPositions, pos)) return pinnedPositions; +// return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, pos)); +// }); +// }, []); + +// // Toggle pin at current position when the editor requests it +// useEvent(ec.events.requestedAction, act => { +// if (act.kind !== 'togglePin') return +// if (!curPos) return +// setPinnedPositions(pinnedPositions => { +// if (isPinned(pinnedPositions, curPos)) { +// return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, curPos)); +// } else { +// pinKey.current += 1; +// return [ ...pinnedPositions, { ...curPos, key: pinKey.current.toString() } ]; +// } +// }); +// }, [curPos?.uri, curPos?.line, curPos?.character]); + +// const infoProps: Keyed[] = pinnedPositions.map(pos => ({ kind: 'pin', onPin: unpin, pos, key: pos.key })); +// if (curPos) infoProps.push({ kind: 'cursor', onPin: pin, key: 'cursor' }); + +// return
+// {infoProps.map (ps => )} +// {!curPos &&

{t("Click somewhere in the Lean file to enable the infoview.")}

} +//
; +// } diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 9a21fab..bb4b244 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -1,43 +1,43 @@ -/* Partly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx */ - -import * as React from 'react'; -import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol'; - -import 'tachyons/css/tachyons.css'; -import '@vscode/codicons/dist/codicon.css'; -import '../../../../node_modules/lean4-infoview/src/infoview/index.css'; -import '../../css/infoview.css' - -import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api'; -import { useClientNotificationEffect, useServerNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util'; -import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; -import { RpcContext, WithRpcSessions, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; -import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infoview/serverVersion'; - -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faDeleteLeft, faHome, faArrowRight, faArrowLeft, faRotateLeft } from '@fortawesome/free-solid-svg-icons' -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' - -import { useAppDispatch, useAppSelector } from '../../hooks'; -import { LevelInfo, useGetGameInfoQuery, useLoadLevelQuery } from '../../state/api'; -import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress'; - -import { Infos } from './infos'; -import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; -import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals'; -import { ChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext, GameIdContext } from '../../state/context'; -import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter'; -import { InteractiveDiagnostic } from '@leanprover/infoview/*'; -import { CircularProgress } from '@mui/material'; -import { GameHint, InteractiveGoalWithHints, InteractiveGoalsWithHints, ProofState } from './rpc_api'; -import { store } from '../../state/store'; -import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; -import { DiagnosticSeverity } from 'vscode-languageclient'; -import { useTranslation } from 'react-i18next'; -import path from 'path'; -import { useContext } from 'react'; -import { Hints, MoreHelpButton, filterHints } from '../chat'; -import { Button, Markdown } from '../utils' +// /* Partly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx */ + +// import * as React from 'react'; +// import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol'; + +// import 'tachyons/css/tachyons.css'; +// import '@vscode/codicons/dist/codicon.css'; +// import '../../../../node_modules/lean4-infoview/src/infoview/index.css'; +// import '../../css/infoview.css' + +// import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api'; +// import { useClientNotificationEffect, useServerNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +// import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; +// import { RpcContext, WithRpcSessions, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; +// import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infoview/serverVersion'; + +// import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +// import { faDeleteLeft, faHome, faArrowRight, faArrowLeft, faRotateLeft } from '@fortawesome/free-solid-svg-icons' +// import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' + +// import { useAppDispatch, useAppSelector } from '../../hooks'; +// import { LevelInfo, useGetGameInfoQuery, useLoadLevelQuery } from '../../state/api'; +// import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress'; + +// import { Infos } from './infos'; +// import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; +// import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals'; +// import { ChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext, GameIdContext } from '../../state/context'; +// import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter'; +// import { InteractiveDiagnostic } from '@leanprover/infoview/*'; +// import { CircularProgress } from '@mui/material'; +// import { GameHint, InteractiveGoalWithHints, InteractiveGoalsWithHints, ProofState } from './rpc_api'; +// import { store } from '../../state/store'; +// import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +// import { DiagnosticSeverity } from 'vscode-languageclient'; +// import { useTranslation } from 'react-i18next'; +// import path from 'path'; +// import { useContext } from 'react'; +// import { Hints, MoreHelpButton, filterHints } from '../chat'; +// import { Button, Markdown } from '../utils' /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is @@ -126,498 +126,498 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin } -/** The mathematical formulation of the statement, supporting e.g. Latex - * It takes three forms, depending on the precence of name and description: - * - Theorem xyz: description - * - Theorem xyz - * - Exercises: description - * - * If `showLeanStatement` is true, it will additionally display the lean code. - */ -export function ExerciseStatement({ showLeanStatement = false }) { - let { t } = useTranslation() - const {gameId, worldId, levelId } = React.useContext(GameIdContext) - const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) - - if (!(levelInfo.data?.descrText || levelInfo.data?.descrFormat)) { return <> } - return <> -
- {levelInfo.data?.descrText ? - - {(levelInfo.data?.displayName ? `**${t("Theorem")}** \`${levelInfo.data?.displayName}\`: ` : '') + t(levelInfo.data?.descrText, {ns: gameId})} - : levelInfo.data?.displayName && - - {`**${t("Theorem")}** \`${levelInfo.data?.displayName}\``} - - } - {levelInfo.data?.descrFormat && showLeanStatement && -

{levelInfo.data?.descrFormat}

- } -
- -} - -// TODO: This is only used in `EditorInterface` -// while `TypewriterInterface` has this copy-pasted in. -export function Main(props: { world: string, level: number, data: LevelInfo}) { - let { t } = useTranslation() - const ec = React.useContext(EditorContext); - const {gameId, worldId, levelId} = React.useContext(GameIdContext) - - const { proof, setProof } = React.useContext(ProofContext) - const {selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp} = React.useContext(ChatContext) - - function toggleSelection(line: number) { - return (ev) => { - console.debug('toggled selection') - if (selectedStep == line) { - setSelectedStep(null) - } else { - setSelectedStep(line) - } - } - } - console.debug(`template: ${props.data?.template}`) - - // React.useEffect (() => { - // if (props.data.template) { - // let code: string = selectCode(gameId, worldId, levelId)(store.getState()) - // if (!code.length) { - // //models.push(monaco.editor.createModel(code, 'lean4', uri)) - // } - // } - // }, [props.data.template]) - - /* Set up updates to the global infoview state on editor events. */ - const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; - - const [allProgress, _1] = useServerNotificationState( - '$/lean/fileProgress', - new Map(), - async (params: LeanFileProgressParams) => (allProgress) => { - const newProgress = new Map(allProgress); - return newProgress.set(params.textDocument.uri, params.processing); - }, - [] - ); - - const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri); - - const curPos: DocumentPosition | undefined = - useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) - - // Effect when the cursor changes in the editor - React.useEffect(() => { - // TODO: this is a bit of a hack and will yield unexpected behaviour if lines - // are indented. - let newPos = curPos?.line + (curPos?.character == 0 ? 0 : 1) - - // scroll the chat along - setSelectedStep(newPos) - }, [curPos]) - - useClientNotificationEffect( - 'textDocument/didClose', - (params: DidCloseTextDocumentParams) => { - if (ec.events.changedCursorLocation.current && - ec.events.changedCursorLocation.current.uri === params.textDocument.uri) { - ec.events.changedCursorLocation.fire(undefined) - } - }, - [] - ); - - const serverVersion = - useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) - const serverStoppedResult = useEventResult(ec.events.serverStopped); - // NB: the cursor may temporarily become `undefined` when a file is closed. In this case - // it's important not to reconstruct the `WithBlah` wrappers below since they contain state - // that we want to persist. - let ret - if (!serverVersion) { - ret =

{t("Waiting for Lean server to start…")}

- } else if (serverStoppedResult) { - ret =

{serverStoppedResult.message}

{serverStoppedResult.reason}

- } else { - ret =
- {proof?.completedWithWarnings && -
- {proof?.completed ? t("Level completed! 🎉") : t("Level completed with warnings 🎭")} -
- } - - {/* - */} -
- } - - return ret -} - -const goalFilter = { - reverse: false, - showType: true, - showInstance: true, - showHiddenAssumption: true, - showLetValue: true -} - -/** The display of a single entered lean command */ -function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) { - let {t} = useTranslation() - - // The first step will always have an empty command - if (!proof?.steps[i]?.command) { return <> } - - if (isLastStepWithErrors(proof, i)) { - // If the last step has errors, we display the command in a different style - // indicating that it will be removed on the next try. - return
- {t("Failed command")}: {proof?.steps[i].command} -
- } else { - return
-
{proof?.steps[i].command}
- -
- } -} - -// const MessageView = React.memo(({uri, diag}: MessageViewProps) => { +// /** The mathematical formulation of the statement, supporting e.g. Latex +// * It takes three forms, depending on the precence of name and description: +// * - Theorem xyz: description +// * - Theorem xyz +// * - Exercises: description +// * +// * If `showLeanStatement` is true, it will additionally display the lean code. +// */ +// export function ExerciseStatement({ showLeanStatement = false }) { +// let { t } = useTranslation() +// const {gameId, worldId, levelId } = React.useContext(GameIdContext) +// const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + +// if (!(levelInfo.data?.descrText || levelInfo.data?.descrFormat)) { return <> } +// return <> +//
+// {levelInfo.data?.descrText ? +// +// {(levelInfo.data?.displayName ? `**${t("Theorem")}** \`${levelInfo.data?.displayName}\`: ` : '') + t(levelInfo.data?.descrText, {ns: gameId})} +// : levelInfo.data?.displayName && +// +// {`**${t("Theorem")}** \`${levelInfo.data?.displayName}\``} +// +// } +// {levelInfo.data?.descrFormat && showLeanStatement && +//

{levelInfo.data?.descrFormat}

+// } +//
+// +// } + +// // TODO: This is only used in `EditorInterface` +// // while `TypewriterInterface` has this copy-pasted in. +// export function Main(props: { world: string, level: number, data: LevelInfo}) { +// let { t } = useTranslation() // const ec = React.useContext(EditorContext); -// const fname = escapeHtml(basename(uri)); -// const {line, character} = diag.range.start; -// const loc: Location = { uri, range: diag.range }; -// const text = TaggedText_stripTags(diag.message); -// const severityClass = diag.severity ? { -// [DiagnosticSeverity.Error]: 'error', -// [DiagnosticSeverity.Warning]: 'warning', -// [DiagnosticSeverity.Information]: 'information', -// [DiagnosticSeverity.Hint]: 'hint', -// }[diag.severity] : ''; -// const title = `Line ${line+1}, Character ${character}`; - -// // Hide "unsolved goals" messages -// let message; -// if ("append" in diag.message && "text" in diag.message.append[0] && -// diag.message?.append[0].text === "unsolved goals") { -// message = diag.message.append[0] +// const {gameId, worldId, levelId} = React.useContext(GameIdContext) + +// const { proof, setProof } = React.useContext(ProofContext) +// const {selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp} = React.useContext(ChatContext) + +// function toggleSelection(line: number) { +// return (ev) => { +// console.debug('toggled selection') +// if (selectedStep == line) { +// setSelectedStep(null) +// } else { +// setSelectedStep(line) +// } +// } +// } +// console.debug(`template: ${props.data?.template}`) + +// // React.useEffect (() => { +// // if (props.data.template) { +// // let code: string = selectCode(gameId, worldId, levelId)(store.getState()) +// // if (!code.length) { +// // //models.push(monaco.editor.createModel(code, 'lean4', uri)) +// // } +// // } +// // }, [props.data.template]) + +// /* Set up updates to the global infoview state on editor events. */ +// const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; + +// const [allProgress, _1] = useServerNotificationState( +// '$/lean/fileProgress', +// new Map(), +// async (params: LeanFileProgressParams) => (allProgress) => { +// const newProgress = new Map(allProgress); +// return newProgress.set(params.textDocument.uri, params.processing); +// }, +// [] +// ); + +// const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri); + +// const curPos: DocumentPosition | undefined = +// useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) + +// // Effect when the cursor changes in the editor +// React.useEffect(() => { +// // TODO: this is a bit of a hack and will yield unexpected behaviour if lines +// // are indented. +// let newPos = curPos?.line + (curPos?.character == 0 ? 0 : 1) + +// // scroll the chat along +// setSelectedStep(newPos) +// }, [curPos]) + +// useClientNotificationEffect( +// 'textDocument/didClose', +// (params: DidCloseTextDocumentParams) => { +// if (ec.events.changedCursorLocation.current && +// ec.events.changedCursorLocation.current.uri === params.textDocument.uri) { +// ec.events.changedCursorLocation.fire(undefined) +// } +// }, +// [] +// ); + +// const serverVersion = +// useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) +// const serverStoppedResult = useEventResult(ec.events.serverStopped); +// // NB: the cursor may temporarily become `undefined` when a file is closed. In this case +// // it's important not to reconstruct the `WithBlah` wrappers below since they contain state +// // that we want to persist. +// let ret +// if (!serverVersion) { +// ret =

{t("Waiting for Lean server to start…")}

+// } else if (serverStoppedResult) { +// ret =

{serverStoppedResult.message}

{serverStoppedResult.reason}

// } else { -// message = diag.message +// ret =
+// {proof?.completedWithWarnings && +//
+// {proof?.completed ? t("Level completed! 🎉") : t("Level completed with warnings 🎭")} +//
+// } +// +// {/* +// */} +//
// } -// const { typewriterMode } = React.useContext(PageContext) - -// return ( -// //
-// // {title} -// // -// // { e.preventDefault(); void ec.revealLocation(loc); }} -// // title="reveal file location"> -// // {e.preventDefault(); void ec.copyToComment(text)}} -// // title="copy message to comment"> -// // {e.preventDefault(); void ec.api.copyToClipboard(text)}} -// // title="copy message to clipboard"> -// // -// // -//
-// {!typewriterMode &&

{title}

} -// 
-//               
-//
-//
-// //
-// ) -// }, fastIsEqual) - -/** The tabs of goals that lean has after the command of this step has been processed */ -export function GoalsTabs({ goals, last, onClick, onGoalChange=(n)=>{}}: { goals: InteractiveGoalWithHints[], last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) { - let { t } = useTranslation() - const [selectedGoal, setSelectedGoal] = React.useState(0) - - if (goals.length == 0) { - return <> - } - - return
-
- {goals.map((goal, i) => ( - // TODO: Should not use index as key. -
{ onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}> - {i ? t("Goal") + ` ${i + 1}` : t("Active Goal")} -
- ))} -
-
- -
-
-} - -// Splitting up Typewriter into two parts is a HACK -export function TypewriterInterfaceWrapper(props: { world: string, level: number, data: LevelInfo, worldSize: number }) { - const ec = React.useContext(EditorContext) - const {gameId} = React.useContext(GameIdContext) - - useClientNotificationEffect( - 'textDocument/didClose', - (params: DidCloseTextDocumentParams) => { - if (ec.events.changedCursorLocation.current && - ec.events.changedCursorLocation.current.uri === params.textDocument.uri) { - ec.events.changedCursorLocation.fire(undefined) - } - }, [] - ) - - const serverVersion = - useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) - const serverStoppedResult = useEventResult(ec.events.serverStopped); - // NB: the cursor may temporarily become `undefined` when a file is closed. In this case - // it's important not to reconstruct the `WithBlah` wrappers below since they contain state - // that we want to persist. - - if (!serverVersion) { return <> } - if (serverStoppedResult) { - return
-

{serverStoppedResult.message}

-

{serverStoppedResult.reason}

-
- } - - return -} - -/** The interface in command line mode */ -export function TypewriterInterface({props}) { - let { t } = useTranslation() - const ec = React.useContext(EditorContext) - const {gameId,worldId, levelId} = React.useContext(GameIdContext) - const editor = React.useContext(MonacoEditorContext) - const model = editor.getModel() - const uri = model.uri.toString() - - const gameInfo = useGetGameInfoQuery({game: gameId}) - let image: string = gameInfo.data?.worlds.nodes[worldId].image - - - const [disableInput, setDisableInput] = React.useState(false) - const [loadingProgress, setLoadingProgress] = React.useState(0) - const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = React.useContext(ChatContext) - const {mobile} = React.useContext(PreferencesContext) - const { proof, setProof, crashed, setCrashed, interimDiags } = React.useContext(ProofContext) - const { setTypewriterInput } = React.useContext(PageContext) - - const proofPanelRef = React.useRef(null) - // 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?.steps.slice(line).map((step, i) => { - let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) - - // Only add these hidden hints to the deletion stack which were visible - deletedChat = [...deletedChat, ...filteredHints.filter(hint => (!hint.hidden || showHelp.has(line + i)))] - }) - setDeletedChat(deletedChat) - - // delete showHelp for deleted steps - setShowHelp(new Set(Array.from(showHelp).filter(i => i < line - 1))) - - editor.executeEdits("typewriter", [{ - range: monaco.Selection.fromPositions( - { lineNumber: line, column: 1 }, - editor.getModel().getFullModelRange().getEndPosition() - ), - text: '', - forceMoveMarkers: false - }]) - setSelectedStep(null) - setTypewriterInput(proof?.steps[line].command) - // Reload proof on deleting - loadGoals(rpcSess, uri, setProof, setCrashed) - ev.stopPropagation() - } - } - - function toggleSelectStep(line: number) { - return (ev) => { - if (mobile) {return} - if (selectedStep == line) { - setSelectedStep(null) - console.debug(`unselected step`) - } else { - setSelectedStep(line) - console.debug(`step ${line} selected`) - } - } - } - - // Scroll to the end of the proof if it is updated. - React.useEffect(() => { - if (proof?.steps.length > 1) { - proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0) - } else { - proofPanelRef.current?.scrollTo(0,0) - } - // also reenable the commandline when the proof changes +// return ret +// } + +// const goalFilter = { +// reverse: false, +// showType: true, +// showInstance: true, +// showHiddenAssumption: true, +// showLetValue: true +// } + +// /** The display of a single entered lean command */ +// function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) { +// let {t} = useTranslation() + +// // The first step will always have an empty command +// if (!proof?.steps[i]?.command) { return <> } + +// if (isLastStepWithErrors(proof, i)) { +// // If the last step has errors, we display the command in a different style +// // indicating that it will be removed on the next try. +// return
+// {t("Failed command")}: {proof?.steps[i].command} +//
+// } else { +// return
+//
{proof?.steps[i].command}
+// +//
+// } +// } + +// // const MessageView = React.memo(({uri, diag}: MessageViewProps) => { +// // const ec = React.useContext(EditorContext); +// // const fname = escapeHtml(basename(uri)); +// // const {line, character} = diag.range.start; +// // const loc: Location = { uri, range: diag.range }; +// // const text = TaggedText_stripTags(diag.message); +// // const severityClass = diag.severity ? { +// // [DiagnosticSeverity.Error]: 'error', +// // [DiagnosticSeverity.Warning]: 'warning', +// // [DiagnosticSeverity.Information]: 'information', +// // [DiagnosticSeverity.Hint]: 'hint', +// // }[diag.severity] : ''; +// // const title = `Line ${line+1}, Character ${character}`; + +// // // Hide "unsolved goals" messages +// // let message; +// // if ("append" in diag.message && "text" in diag.message.append[0] && +// // diag.message?.append[0].text === "unsolved goals") { +// // message = diag.message.append[0] +// // } else { +// // message = diag.message +// // } + +// // const { typewriterMode } = React.useContext(PageContext) + +// // return ( +// // //
+// // // {title} +// // // +// // // { e.preventDefault(); void ec.revealLocation(loc); }} +// // // title="reveal file location"> +// // // {e.preventDefault(); void ec.copyToComment(text)}} +// // // title="copy message to comment"> +// // // {e.preventDefault(); void ec.api.copyToClipboard(text)}} +// // // title="copy message to clipboard"> +// // // +// // // +// //
+// // {!typewriterMode &&

{title}

} +// // 
+// //               
+// //
+// //
+// // //
+// // ) +// // }, fastIsEqual) + +// /** The tabs of goals that lean has after the command of this step has been processed */ +// export function GoalsTabs({ goals, last, onClick, onGoalChange=(n)=>{}}: { goals: InteractiveGoalWithHints[], last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) { +// let { t } = useTranslation() +// const [selectedGoal, setSelectedGoal] = React.useState(0) + +// if (goals.length == 0) { +// return <> +// } - // BUG: If selecting 2nd goal on a intermediate proofstep and then delete proof to there, - // the commandline is not displaying disabled even though it should. - setDisableInput(false) - }, [proof]) +// return
+//
+// {goals.map((goal, i) => ( +// // TODO: Should not use index as key. +//
{ onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}> +// {i ? t("Goal") + ` ${i + 1}` : t("Active Goal")} +//
+// ))} +//
+//
+// +//
+//
+// } + +// // Splitting up Typewriter into two parts is a HACK +// export function TypewriterInterfaceWrapper(props: { world: string, level: number, data: LevelInfo, worldSize: number }) { +// const ec = React.useContext(EditorContext) +// const {gameId} = React.useContext(GameIdContext) + +// useClientNotificationEffect( +// 'textDocument/didClose', +// (params: DidCloseTextDocumentParams) => { +// if (ec.events.changedCursorLocation.current && +// ec.events.changedCursorLocation.current.uri === params.textDocument.uri) { +// ec.events.changedCursorLocation.fire(undefined) +// } +// }, [] +// ) - // Scroll to element if selection changes - React.useEffect(() => { - if (typeof selectedStep !== 'undefined') { - Array.from(proofPanelRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { - elem.scrollIntoView({ block: "center" }) - }) - } - }, [selectedStep]) +// const serverVersion = +// useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) +// const serverStoppedResult = useEventResult(ec.events.serverStopped); +// // NB: the cursor may temporarily become `undefined` when a file is closed. In this case +// // it's important not to reconstruct the `WithBlah` wrappers below since they contain state +// // that we want to persist. + +// if (!serverVersion) { return <> } +// if (serverStoppedResult) { +// return
+//

{serverStoppedResult.message}

+//

{serverStoppedResult.reason}

+//
+// } - // TODO: superfluous, can be replaced with `withErr` from above - let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false +// return +// } + +// /** The interface in command line mode */ +// export function TypewriterInterface({props}) { +// let { t } = useTranslation() +// const ec = React.useContext(EditorContext) +// const {gameId,worldId, levelId} = React.useContext(GameIdContext) +// const editor = React.useContext(MonacoEditorContext) +// const model = editor.getModel() +// const uri = model.uri.toString() + +// const gameInfo = useGetGameInfoQuery({game: gameId}) +// let image: string = gameInfo.data?.worlds.nodes[worldId].image + + +// const [disableInput, setDisableInput] = React.useState(false) +// const [loadingProgress, setLoadingProgress] = React.useState(0) +// const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = React.useContext(ChatContext) +// const {mobile} = React.useContext(PreferencesContext) +// const { proof, setProof, crashed, setCrashed, interimDiags } = React.useContext(ProofContext) +// const { setTypewriterInput } = React.useContext(PageContext) + +// const proofPanelRef = React.useRef(null) +// // 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?.steps.slice(line).map((step, i) => { +// let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) + +// // Only add these hidden hints to the deletion stack which were visible +// deletedChat = [...deletedChat, ...filteredHints.filter(hint => (!hint.hidden || showHelp.has(line + i)))] +// }) +// setDeletedChat(deletedChat) + +// // delete showHelp for deleted steps +// setShowHelp(new Set(Array.from(showHelp).filter(i => i < line - 1))) + +// editor.executeEdits("typewriter", [{ +// range: monaco.Selection.fromPositions( +// { lineNumber: line, column: 1 }, +// editor.getModel().getFullModelRange().getEndPosition() +// ), +// text: '', +// forceMoveMarkers: false +// }]) +// setSelectedStep(null) +// setTypewriterInput(proof?.steps[line].command) +// // Reload proof on deleting +// loadGoals(rpcSess, uri, setProof, setCrashed) +// ev.stopPropagation() +// } +// } +// function toggleSelectStep(line: number) { +// return (ev) => { +// if (mobile) {return} +// if (selectedStep == line) { +// setSelectedStep(null) +// console.debug(`unselected step`) +// } else { +// setSelectedStep(line) +// console.debug(`step ${line} selected`) +// } +// } +// } - useServerNotificationEffect("$/game/loading", (params : any) => { - if (params.kind == "loadConstants") { - setLoadingProgress(params.counter/100*50) - } else if (params.kind == "finalizeExtensions") { - setLoadingProgress(50 + params.counter/150*50) - } else { - console.error(`Unknown loading kind: ${params.kind}`) - } - }) - - return
- -
- {/*
- {image && - - } - -
*/} - {/*
-
- -
-
*/} -
- {/* */} - {crashed ?
-

{t("Crashed! Go to editor mode and fix your proof! Last server response:")}

- {interimDiags.map(diag => { - const severityClass = diag.severity ? { - [DiagnosticSeverity.Error]: 'error', - [DiagnosticSeverity.Warning]: 'warning', - [DiagnosticSeverity.Information]: 'information', - [DiagnosticSeverity.Hint]: 'hint', - }[diag.severity] : ''; - - return
-
-

{t("Line")} {diag.range.start.line}, {t("Character")} {diag.range.start.character}

- 
-                  {diag.message}
-
-
-
- })} - -
: proof?.steps.length ? - <> - {proof?.steps.map((step, i) => { - let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) - - // if (i == proof?.steps.length - 1 && hasInteractiveErrors(step.diags)) { - // // if the last command contains an error, we only display the errors but not the - // // entered command as it is still present in the command line. - // // TODO: Should not use index as key. - // return
- // - //
- // } else { - return
- {i > 0 && <> - - - } - {mobile && i == 0 && props.data?.introduction && -
- {props.data?.introduction} -
- } - {mobile && - ({hint: hint, step: i}))} /> - } - {/* setDisableInput(n > 0) : (n) => {}}/> */} - {!(isLastStepWithErrors(proof, i)) && - setDisableInput(n > 0) : (n) => {}}/> - } - {mobile && i == proof?.steps.length - 1 && - - } - - {/* Show a message that there are no goals left */} - {/* {!step.goals.length && ( -
- {proof?.completed ? -

Level completed! 🎉

: -

- no goals left
- This probably means you solved the level with warnings or Lean encountered a parsing error. -

- } -
- )} */} -
- } - //} - )} - {proof?.diagnostics.length > 0 && -
- -
- } - {mobile && proof?.completed && -
- {props.level >= props.worldSize ? - - : - - } -
- } - : - // note: since we don't know the total number of files, - // we use a function which strictly monotonely increases towards `100` as `x → ∞` - // The base is chosen at random s.t. we get roughly 91% for `x = 100`. - } -
-
- - -
-} +// // Scroll to the end of the proof if it is updated. +// React.useEffect(() => { +// if (proof?.steps.length > 1) { +// proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0) +// } else { +// proofPanelRef.current?.scrollTo(0,0) +// } +// // also reenable the commandline when the proof changes + +// // BUG: If selecting 2nd goal on a intermediate proofstep and then delete proof to there, +// // the commandline is not displaying disabled even though it should. +// setDisableInput(false) +// }, [proof]) + +// // Scroll to element if selection changes +// React.useEffect(() => { +// if (typeof selectedStep !== 'undefined') { +// Array.from(proofPanelRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { +// elem.scrollIntoView({ block: "center" }) +// }) +// } +// }, [selectedStep]) + +// // TODO: superfluous, can be replaced with `withErr` from above +// let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false + + +// useServerNotificationEffect("$/game/loading", (params : any) => { +// if (params.kind == "loadConstants") { +// setLoadingProgress(params.counter/100*50) +// } else if (params.kind == "finalizeExtensions") { +// setLoadingProgress(50 + params.counter/150*50) +// } else { +// console.error(`Unknown loading kind: ${params.kind}`) +// } +// }) + +// return
+// +//
+// {/*
+// {image && +// +// } + +//
*/} +// {/*
+//
+ +//
+//
*/} +//
+// {/* */} +// {crashed ?
+//

{t("Crashed! Go to editor mode and fix your proof! Last server response:")}

+// {interimDiags.map(diag => { +// const severityClass = diag.severity ? { +// [DiagnosticSeverity.Error]: 'error', +// [DiagnosticSeverity.Warning]: 'warning', +// [DiagnosticSeverity.Information]: 'information', +// [DiagnosticSeverity.Hint]: 'hint', +// }[diag.severity] : ''; + +// return
+//
+//

{t("Line")} {diag.range.start.line}, {t("Character")} {diag.range.start.character}

+// 
+//                   {diag.message}
+//
+//
+//
+// })} + +//
: proof?.steps.length ? +// <> +// {proof?.steps.map((step, i) => { +// let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) + +// // if (i == proof?.steps.length - 1 && hasInteractiveErrors(step.diags)) { +// // // if the last command contains an error, we only display the errors but not the +// // // entered command as it is still present in the command line. +// // // TODO: Should not use index as key. +// // return
+// // +// //
+// // } else { +// return
+// {i > 0 && <> +// +// +// } +// {mobile && i == 0 && props.data?.introduction && +//
+// {props.data?.introduction} +//
+// } +// {mobile && +// ({hint: hint, step: i}))} /> +// } +// {/* setDisableInput(n > 0) : (n) => {}}/> */} +// {!(isLastStepWithErrors(proof, i)) && +// setDisableInput(n > 0) : (n) => {}}/> +// } +// {mobile && i == proof?.steps.length - 1 && +// +// } + +// {/* Show a message that there are no goals left */} +// {/* {!step.goals.length && ( +//
+// {proof?.completed ? +//

Level completed! 🎉

: +//

+// no goals left
+// This probably means you solved the level with warnings or Lean encountered a parsing error. +//

+// } +//
+// )} */} +//
+// } +// //} +// )} +// {proof?.diagnostics.length > 0 && +//
+// +//
+// } +// {mobile && proof?.completed && +//
+// {props.level >= props.worldSize ? +// +// : +// +// } +//
+// } +// : +// // note: since we don't know the total number of files, +// // we use a function which strictly monotonely increases towards `100` as `x → ∞` +// // The base is chosen at random s.t. we get roughly 91% for `x = 100`. +// } +//
+//
+// +// +//
+// } diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx index c1c8f13..420a1e9 100644 --- a/client/src/components/infoview/messages.tsx +++ b/client/src/components/infoview/messages.tsx @@ -1,240 +1,240 @@ -import * as React from 'react' -import fastIsEqual from 'react-fast-compare' -import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol' - -import { LeanDiagnostic, RpcErrorCode, getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api' - -import { basename, escapeHtml, usePausableState, useEvent, addUniqueKeys, DocumentPosition, useServerNotificationState, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util' -import { ConfigContext, EditorContext, LspDiagnosticsContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts' -import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/collapsing' -import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer' -import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions' - -import { PageContext } from '../../state/context' -import { useTranslation } from 'react-i18next' - -interface MessageViewProps { - uri: DocumentUri; - diag: InteractiveDiagnostic; -} - -/** A list of messages (info/warning/error) that are produced after this command */ -function Error({error, typewriterMode} : {error : InteractiveDiagnostic, typewriterMode : boolean}) { - // The first step will always have an empty command - - const severityClass = error.severity ? { - [DiagnosticSeverity.Error]: 'error', - [DiagnosticSeverity.Warning]: 'warning', - [DiagnosticSeverity.Information]: 'information', - [DiagnosticSeverity.Hint]: 'hint', - }[error.severity] : ''; - - const {line, character} = error.range.start; - const title = `Line ${line+1}, Character ${character}`; - - // Hide "unsolved goals" messages - let message; - if ("append" in error.message && "text" in error.message.append[0] && - error.message?.append[0].text === "unsolved goals") { - message = error.message.append[0] - } else { - message = error.message - } - - return
- {!typewriterMode &&

{title}

} - 
-      
-
-
-} - -// TODO: Should not use index as key. -/** A list of messages (info/warning/error) that are produced after this command */ -export function Errors ({errors, typewriterMode} : {errors : InteractiveDiagnostic[], typewriterMode : boolean}) { - return
- {errors.map((err, i) => ())} -
-} - -const MessageView = React.memo(({uri, diag}: MessageViewProps) => { - const ec = React.useContext(EditorContext); - const fname = escapeHtml(basename(uri)); - const {line, character} = diag.range.start; - const loc: Location = { uri, range: diag.range }; - const text = TaggedText_stripTags(diag.message); - const severityClass = diag.severity ? { - [DiagnosticSeverity.Error]: 'error', - [DiagnosticSeverity.Warning]: 'warning', - [DiagnosticSeverity.Information]: 'information', - [DiagnosticSeverity.Hint]: 'hint', - }[diag.severity] : ''; - const title = `Line ${line+1}, Character ${character}`; - - // Hide "unsolved goals" messages - let message; - if ("append" in diag.message && "text" in diag.message.append[0] && - diag.message?.append[0].text === "unsolved goals") { - message = diag.message.append[0] - } else { - message = diag.message - } - - const { typewriterMode, lockEditorMode } = React.useContext(PageContext) - - return ( - //
- // {title} - // - // { e.preventDefault(); void ec.revealLocation(loc); }} - // title="reveal file location"> - // {e.preventDefault(); void ec.copyToComment(text)}} - // title="copy message to comment"> - // {e.preventDefault(); void ec.api.copyToClipboard(text)}} - // title="copy message to clipboard"> - // - // -
- {!(typewriterMode && !lockEditorMode) &&

{title}

} - 
-                
-
-
- //
- ) -}, fastIsEqual) - -function mkMessageViewProps(uri: DocumentUri, messages: InteractiveDiagnostic[]): MessageViewProps[] { - const views: MessageViewProps[] = messages - .sort((msga, msgb) => { - const a = msga.fullRange?.end || msga.range.end; - const b = msgb.fullRange?.end || msgb.range.end; - return a.line === b.line ? a.character - b.character : a.line - b.line - }).map(m => { - return { uri, diag: m }; - }); - - return addUniqueKeys(views, v => DocumentPosition.toString({uri: v.uri, ...v.diag.range.start})); -} - -/** Shows the given messages assuming they are for the given file. */ -export const MessagesList = React.memo(({uri, messages}: {uri: DocumentUri, messages: InteractiveDiagnostic[]}) => { - const should_hide = messages.length === 0; - if (should_hide) { return <> } - - return ( -
- {mkMessageViewProps(uri, messages).map(m => )} -
- ); -}) - -function lazy(f: () => T): () => T { - let state: {t: T} | undefined - return () => { - if (!state) state = {t: f()} - return state.t - } -} - -/** Displays all messages for the specified file. Can be paused. */ -export function AllMessages() { - const ec = React.useContext(EditorContext); - const sv = React.useContext(VersionContext); - const curPos: DocumentPosition | undefined = - useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) - const rs0 = useRpcSessionAtPos({ uri: curPos.uri, line: 0, character: 0 }); - const dc = React.useContext(LspDiagnosticsContext); - const config = React.useContext(ConfigContext); - const diags0 = dc.get(curPos.uri) || []; - - const iDiags0 = React.useMemo(() => lazy(async () => { - try { - const diags = await getInteractiveDiagnostics(rs0); - if (diags.length > 0) { - return diags - } - } catch (err: any) { - if (err?.code === RpcErrorCode.ContentModified) { - // Document has been changed since we made the request. This can happen - // while typing quickly. When the server catches up on next edit, it will - // send new diagnostics to which the infoview responds by calling - // `getInteractiveDiagnostics` again. - } else { - console.log('getInteractiveDiagnostics error ', err) - } - } - return diags0.map(d => ({ ...(d as LeanDiagnostic), message: { text: d.message } })); - }), [sv, rs0, curPos.uri, diags0]); - const [{ isPaused, setPaused }, [uri, rs, diags, iDiags], _] = usePausableState(false, [curPos.uri, rs0, diags0, iDiags0]); - - // Fetch interactive diagnostics when we're entering the paused state - // (if they haven't already been fetched before) - React.useEffect(() => { if (isPaused) { void iDiags() } }, [iDiags, isPaused]); - - const setOpenRef = React.useRef>>(); - useEvent(ec.events.requestedAction, act => { - if (act.kind === 'toggleAllMessages' && setOpenRef.current !== undefined) { - setOpenRef.current(t => !t); - } - }); - - return ( - - {/*
- - All Messages ({diags.length}) - - { e.preventDefault(); setPaused(p => !p); }} - title={isPaused ? 'continue updating' : 'pause updating'}> - - - */} - - {/*
*/} - - ) -} - -/** We factor out the body of {@link AllMessages} which lazily fetches its contents only when expanded. */ -function AllMessagesBody({uri, curPos, messages}: {uri: DocumentUri, curPos: DocumentPosition | undefined , messages: () => Promise}) { - let { t } = useTranslation() - const [msgs, setMsgs] = React.useState(undefined) - React.useEffect(() => { void messages().then( - msgs => setMsgs(msgs.filter( - (d)=>{ - //console.log(`message start: ${d.range.start.line}. CurPos: ${curPos.line}`) - - // Only show the messages from the line where the cursor is. - return d.range.start.line == curPos.line - })) - ) }, [messages, curPos]) - if (msgs === undefined) return
{t("Loading messages…")}
- else return -} - -/** - * Provides a `LspDiagnosticsContext` which stores the latest version of the - * diagnostics as sent by the publishDiagnostics notification. - */ -export function WithLspDiagnosticsContext({children}: React.PropsWithChildren<{}>) { - const [allDiags, _0] = useServerNotificationState( - 'textDocument/publishDiagnostics', - new Map(), - async (params: PublishDiagnosticsParams) => diags => - new Map(diags).set(params.uri, params.diagnostics), - [] - ) - - return {children} -} - -/** Embeds a non-interactive diagnostic into the type `InteractiveDiagnostic`. */ -export function lspDiagToInteractive(diag: Diagnostic): InteractiveDiagnostic { - return { ...(diag as LeanDiagnostic), message: { text: diag.message } }; -} +// import * as React from 'react' +// import fastIsEqual from 'react-fast-compare' +// import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol' + +// import { LeanDiagnostic, RpcErrorCode, getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api' + +// import { basename, escapeHtml, usePausableState, useEvent, addUniqueKeys, DocumentPosition, useServerNotificationState, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util' +// import { ConfigContext, EditorContext, LspDiagnosticsContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts' +// import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/collapsing' +// import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer' +// import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions' + +// import { PageContext } from '../../state/context' +// import { useTranslation } from 'react-i18next' + +// interface MessageViewProps { +// uri: DocumentUri; +// diag: InteractiveDiagnostic; +// } + +// /** A list of messages (info/warning/error) that are produced after this command */ +// function Error({error, typewriterMode} : {error : InteractiveDiagnostic, typewriterMode : boolean}) { +// // The first step will always have an empty command + +// const severityClass = error.severity ? { +// [DiagnosticSeverity.Error]: 'error', +// [DiagnosticSeverity.Warning]: 'warning', +// [DiagnosticSeverity.Information]: 'information', +// [DiagnosticSeverity.Hint]: 'hint', +// }[error.severity] : ''; + +// const {line, character} = error.range.start; +// const title = `Line ${line+1}, Character ${character}`; + +// // Hide "unsolved goals" messages +// let message; +// if ("append" in error.message && "text" in error.message.append[0] && +// error.message?.append[0].text === "unsolved goals") { +// message = error.message.append[0] +// } else { +// message = error.message +// } + +// return
+// {!typewriterMode &&

{title}

} +// 
+//       
+//
+//
+// } + +// // TODO: Should not use index as key. +// /** A list of messages (info/warning/error) that are produced after this command */ +// export function Errors ({errors, typewriterMode} : {errors : InteractiveDiagnostic[], typewriterMode : boolean}) { +// return
+// {errors.map((err, i) => ())} +//
+// } + +// const MessageView = React.memo(({uri, diag}: MessageViewProps) => { +// const ec = React.useContext(EditorContext); +// const fname = escapeHtml(basename(uri)); +// const {line, character} = diag.range.start; +// const loc: Location = { uri, range: diag.range }; +// const text = TaggedText_stripTags(diag.message); +// const severityClass = diag.severity ? { +// [DiagnosticSeverity.Error]: 'error', +// [DiagnosticSeverity.Warning]: 'warning', +// [DiagnosticSeverity.Information]: 'information', +// [DiagnosticSeverity.Hint]: 'hint', +// }[diag.severity] : ''; +// const title = `Line ${line+1}, Character ${character}`; + +// // Hide "unsolved goals" messages +// let message; +// if ("append" in diag.message && "text" in diag.message.append[0] && +// diag.message?.append[0].text === "unsolved goals") { +// message = diag.message.append[0] +// } else { +// message = diag.message +// } + +// const { typewriterMode, lockEditorMode } = React.useContext(PageContext) + +// return ( +// //
+// // {title} +// // +// // { e.preventDefault(); void ec.revealLocation(loc); }} +// // title="reveal file location"> +// // {e.preventDefault(); void ec.copyToComment(text)}} +// // title="copy message to comment"> +// // {e.preventDefault(); void ec.api.copyToClipboard(text)}} +// // title="copy message to clipboard"> +// // +// // +//
+// {!(typewriterMode && !lockEditorMode) &&

{title}

} +// 
+//                 
+//
+//
+// //
+// ) +// }, fastIsEqual) + +// function mkMessageViewProps(uri: DocumentUri, messages: InteractiveDiagnostic[]): MessageViewProps[] { +// const views: MessageViewProps[] = messages +// .sort((msga, msgb) => { +// const a = msga.fullRange?.end || msga.range.end; +// const b = msgb.fullRange?.end || msgb.range.end; +// return a.line === b.line ? a.character - b.character : a.line - b.line +// }).map(m => { +// return { uri, diag: m }; +// }); + +// return addUniqueKeys(views, v => DocumentPosition.toString({uri: v.uri, ...v.diag.range.start})); +// } + +// /** Shows the given messages assuming they are for the given file. */ +// export const MessagesList = React.memo(({uri, messages}: {uri: DocumentUri, messages: InteractiveDiagnostic[]}) => { +// const should_hide = messages.length === 0; +// if (should_hide) { return <> } + +// return ( +//
+// {mkMessageViewProps(uri, messages).map(m => )} +//
+// ); +// }) + +// function lazy(f: () => T): () => T { +// let state: {t: T} | undefined +// return () => { +// if (!state) state = {t: f()} +// return state.t +// } +// } + +// /** Displays all messages for the specified file. Can be paused. */ +// export function AllMessages() { +// const ec = React.useContext(EditorContext); +// const sv = React.useContext(VersionContext); +// const curPos: DocumentPosition | undefined = +// useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) +// const rs0 = useRpcSessionAtPos({ uri: curPos.uri, line: 0, character: 0 }); +// const dc = React.useContext(LspDiagnosticsContext); +// const config = React.useContext(ConfigContext); +// const diags0 = dc.get(curPos.uri) || []; + +// const iDiags0 = React.useMemo(() => lazy(async () => { +// try { +// const diags = await getInteractiveDiagnostics(rs0); +// if (diags.length > 0) { +// return diags +// } +// } catch (err: any) { +// if (err?.code === RpcErrorCode.ContentModified) { +// // Document has been changed since we made the request. This can happen +// // while typing quickly. When the server catches up on next edit, it will +// // send new diagnostics to which the infoview responds by calling +// // `getInteractiveDiagnostics` again. +// } else { +// console.log('getInteractiveDiagnostics error ', err) +// } +// } +// return diags0.map(d => ({ ...(d as LeanDiagnostic), message: { text: d.message } })); +// }), [sv, rs0, curPos.uri, diags0]); +// const [{ isPaused, setPaused }, [uri, rs, diags, iDiags], _] = usePausableState(false, [curPos.uri, rs0, diags0, iDiags0]); + +// // Fetch interactive diagnostics when we're entering the paused state +// // (if they haven't already been fetched before) +// React.useEffect(() => { if (isPaused) { void iDiags() } }, [iDiags, isPaused]); + +// const setOpenRef = React.useRef>>(); +// useEvent(ec.events.requestedAction, act => { +// if (act.kind === 'toggleAllMessages' && setOpenRef.current !== undefined) { +// setOpenRef.current(t => !t); +// } +// }); + +// return ( +// +// {/*
+// +// All Messages ({diags.length}) +// +// { e.preventDefault(); setPaused(p => !p); }} +// title={isPaused ? 'continue updating' : 'pause updating'}> +// +// +// */} +// +// {/*
*/} +// +// ) +// } + +// /** We factor out the body of {@link AllMessages} which lazily fetches its contents only when expanded. */ +// function AllMessagesBody({uri, curPos, messages}: {uri: DocumentUri, curPos: DocumentPosition | undefined , messages: () => Promise}) { +// let { t } = useTranslation() +// const [msgs, setMsgs] = React.useState(undefined) +// React.useEffect(() => { void messages().then( +// msgs => setMsgs(msgs.filter( +// (d)=>{ +// //console.log(`message start: ${d.range.start.line}. CurPos: ${curPos.line}`) + +// // Only show the messages from the line where the cursor is. +// return d.range.start.line == curPos.line +// })) +// ) }, [messages, curPos]) +// if (msgs === undefined) return
{t("Loading messages…")}
+// else return +// } + +// /** +// * Provides a `LspDiagnosticsContext` which stores the latest version of the +// * diagnostics as sent by the publishDiagnostics notification. +// */ +// export function WithLspDiagnosticsContext({children}: React.PropsWithChildren<{}>) { +// const [allDiags, _0] = useServerNotificationState( +// 'textDocument/publishDiagnostics', +// new Map(), +// async (params: PublishDiagnosticsParams) => diags => +// new Map(diags).set(params.uri, params.diagnostics), +// [] +// ) + +// return {children} +// } + +// /** Embeds a non-interactive diagnostic into the type `InteractiveDiagnostic`. */ +// export function lspDiagToInteractive(diag: Diagnostic): InteractiveDiagnostic { +// return { ...(diag as LeanDiagnostic), message: { text: diag.message } }; +// } diff --git a/client/src/components/infoview/rpc_api.ts b/client/src/components/infoview/rpc_api.ts index bf15a1b..def6aeb 100644 --- a/client/src/components/infoview/rpc_api.ts +++ b/client/src/components/infoview/rpc_api.ts @@ -4,8 +4,8 @@ * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts` */ import type { Range } from 'vscode-languageserver-protocol'; -import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api'; -import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*'; +// import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api'; +// import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*'; import type { Diagnostic } from 'vscode-languageserver-protocol'; export interface InteractiveHypothesisBundle { @@ -13,9 +13,9 @@ export interface InteractiveHypothesisBundle { * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end. * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */ names: string[]; - fvarIds?: FVarId[]; - type: CodeWithInfos; - val?: CodeWithInfos; + fvarIds?: any // FVarId[]; + type: any // CodeWithInfos; + val?: any // CodeWithInfos; isInstance?: boolean; isType?: boolean; isInserted?: boolean; @@ -25,14 +25,14 @@ export interface InteractiveHypothesisBundle { export interface InteractiveGoalCore { hyps: InteractiveHypothesisBundle[]; - type: CodeWithInfos; - ctx?: ContextInfo; + type: any // CodeWithInfos; + ctx?: any // ContextInfo; } export interface InteractiveGoal extends InteractiveGoalCore { userName?: string; goalPrefix?: string; - mvarId?: MVarId; + mvarId?: any // MVarId; isInserted?: boolean; isRemoved?: boolean; } @@ -43,7 +43,7 @@ export interface InteractiveGoals extends InteractiveGoalCore { export interface InteractiveTermGoal extends InteractiveGoalCore { range?: Range; - term?: TermInfo; + term?: any //TermInfo; } export interface GameHint { @@ -61,7 +61,7 @@ export interface InteractiveGoalWithHints { export interface InteractiveGoalsWithHints { goals: InteractiveGoalWithHints[]; command: string; - diags: InteractiveDiagnostic[]; + diags: any //InteractiveDiagnostic[]; } /** @@ -78,7 +78,7 @@ export interface ProofState { /** The remaining diagnostics that are not in the steps. Usually this should only * be the "unsolved goals" message, I believe. */ - diagnostics : InteractiveDiagnostic[]; + diagnostics : any // InteractiveDiagnostic[]; completed : Boolean; completedWithWarnings : Boolean; } diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx index 211b8d3..5f76285 100644 --- a/client/src/components/infoview/typewriter.tsx +++ b/client/src/components/infoview/typewriter.tsx @@ -1,304 +1,304 @@ -import * as React from 'react' -import { useRef, useState, useEffect } from 'react' -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons' -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { Registry } from 'monaco-textmate' // peer dependency -import { wireTmGrammars } from 'monaco-editor-textmate' -import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol'; -import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util'; -import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter'; -import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider'; -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'; -import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } from '@leanprover/infoview-api'; -import { Diagnostic } from 'vscode-languageserver-types'; -import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; -import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; -import { ChatContext, PageContext, MonacoEditorContext, ProofContext, GameIdContext } from '../../state/context' -import { goalsToString, lastStepHasErrors, loadGoals } from './goals' -import { GameHint, ProofState } from './rpc_api' -import { useTranslation } from 'react-i18next' -import { InputAbbreviationRewriter } from '@leanprover/unicode-input-component' -import ContentEditable from 'react-contenteditable' - -export interface GameDiagnosticsParams { - uri: DocumentUri; - diagnostics: Diagnostic[]; -} - -/* 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'] -}) - -// register Monaco languages // TODO: JE. I dont understand why I suddenly had to add this when it worked without before. -monaco.languages.register({ - id: 'lean4', - extensions: ['.lean'] -}) - -// 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); - -/** The input field */ -export function Typewriter({disabled}: {disabled?: boolean}) { - let { t } = useTranslation() - - /** Reference to the hidden multi-line editor */ - const editor = React.useContext(MonacoEditorContext) - const model = editor?.getModel() - const uri = model?.uri.toString() - - const [oneLineEditor, setOneLineEditor] = useState(null) - const [processing, setProcessing] = useState(false) - - const {typewriterInput, setTypewriterInput} = React.useContext(PageContext) - - const inputRef = useRef() - - // The context storing all information about the current proof - const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext) - - const {gameId, worldId, levelId} = React.useContext(GameIdContext) - - // state to store the last batch of deleted messages - const {setDeletedChat} = React.useContext(ChatContext) - - const rpcSess = React.useContext(RpcContext) - - // Run the command - const runCommand = React.useCallback(() => { - if (processing) {return} - - // TODO: Desired logic is to only reset this after a new *error-free* command has been entered - setDeletedChat([]) - - const pos = editor?.getPosition() - if (typewriterInput) { - setProcessing(true) - editor?.executeEdits("typewriter", [{ - range: monaco.Selection.fromPositions( - pos, - editor?.getModel()?.getFullModelRange()?.getEndPosition() - ), - text: typewriterInput.trim() + "\n", - forceMoveMarkers: false - }]) - setTypewriterInput('') - // Load proof after executing edits - loadGoals(rpcSess, uri, setProof, setCrashed) - } - - editor?.setPosition(pos) - }, [typewriterInput, editor]) - - useEffect(() => { - if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) { - oneLineEditor.setValue(typewriterInput) - } - }, [typewriterInput]) - - /* Load proof on start/switching to typewriter */ - useEffect(() => { - setProof(null) - loadGoals(rpcSess, uri, setProof, setCrashed) - }, [gameId, worldId, levelId]) - - /** If the last step has an error, add the command to the typewriter. */ - useEffect(() => { - if (lastStepHasErrors(proof)) { - setTypewriterInput(proof?.steps[proof?.steps.length - 1].command) - } - }, [proof]) - - // React when answer from the server comes back - useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => { - if (params.uri == uri) { - setProcessing(false) - - console.log('Received lean diagnostics') - console.log(params.diagnostics) - setInterimDiags(params.diagnostics) - - //loadGoals(rpcSess, uri, setProof) - - // TODO: loadAllGoals() - if (!hasErrors(params.diagnostics)) { - //setTypewriterInput("") - editor?.setPosition(editor?.getModel()?.getFullModelRange()?.getEndPosition()) - } - } else { - // console.debug(`expected uri: ${uri}, got: ${params.uri}`) - // console.debug(params) - } - // 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]); - - // // React when answer from the server comes back - // useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => { - // console.log('Received game diagnostics') - // console.log(`diag. uri : ${params.uri}`) - // console.log(params.diagnostics) - - // }, [uri]); - - useEffect(() => { - const myEditor = monaco.editor.create(inputRef.current!, { - value: typewriterInput, - language: "lean4cmd", - quickSuggestions: false, - lightbulb: { - enabled: true - }, - unicodeHighlight: { - ambiguousCharacters: false, - }, - automaticLayout: true, - minimap: { - enabled: false - }, - lineNumbers: 'off', - tabSize: 2, - glyphMargin: false, - folding: false, - lineDecorationsWidth: 0, - lineNumbersMinChars: 0, - 'semanticHighlighting.enabled': true, - overviewRulerLanes: 0, - hideCursorInOverviewRuler: true, - scrollbar: { - vertical: 'hidden', - horizontalScrollbarSize: 3 - }, - overviewRulerBorder: false, - theme: 'vs-code-theme-converted', - fontFamily: "JuliaMono", - contextmenu: false - }) - - 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() - setTypewriterInput(value) - const newValue = value.replace(/[\n\r]/g, '') - if (value != newValue) { - oneLineEditor.setValue(newValue) - } - }) - return () => { l.dispose() } - }, [oneLineEditor, setTypewriterInput]) - - useEffect(() => { - if (!oneLineEditor) return - // Run command when pressing enter - const l = oneLineEditor.onKeyUp((ev) => { - if (ev.code === "Enter" || ev.code === "NumpadEnter") { - runCommand() - } - }) - return () => { l.dispose() } - }, [oneLineEditor, runCommand]) - - // 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) - // console.debug('LOAD ALL GOALS') - // TODO: loadAllGoals() - }, [rpcSess]) - - /** Process the entered command */ - const handleSubmit : React.FormEventHandler = (ev) => { - ev.preventDefault() - runCommand() - } - - // do not display if the proof is completed (with potential warnings still present) - return
-
-
-
-
- - -
-} - -/** Checks whether the diagnostics contain any errors or warnings to check whether the level has - been completed.*/ -export function hasErrors(diags: Diagnostic[]) { - return diags.some( - (d) => - !d.message.startsWith("unsolved goals") && - (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning - ) -} - -// TODO: Didn't manage to unify this with the one above -export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) { - return (typeof diags !== 'undefined') && diags.some( - (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning - ) -} - -export function getInteractiveDiagsAt (proof: ProofState, k : number) { - if (k == 0) { - return [] - } else if (k >= proof?.steps.length-1) { - // TODO: Do we need that? - return proof?.diagnostics.filter(msg => msg.range.start.line >= proof?.steps.length-1) - } else { - return proof?.diagnostics.filter(msg => msg.range.start.line == k-1) - } -} +// import * as React from 'react' +// import { useRef, useState, useEffect } from 'react' +// import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +// import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons' +// import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' +// // import { Registry } from 'monaco-textmate' // peer dependency +// // import { wireTmGrammars } from 'monaco-editor-textmate' +// import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol'; +// import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +// // import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter'; +// // import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider'; +// // 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'; +// import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } from '@leanprover/infoview-api'; +// import { Diagnostic } from 'vscode-languageserver-types'; +// import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +// import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; +// import { ChatContext, PageContext, MonacoEditorContext, ProofContext, GameIdContext } from '../../state/context' +// import { goalsToString, lastStepHasErrors, loadGoals } from './goals' +// import { GameHint, ProofState } from './rpc_api' +// import { useTranslation } from 'react-i18next' +// import { InputAbbreviationRewriter } from '@leanprover/unicode-input-component' +// import ContentEditable from 'react-contenteditable' + +// export interface GameDiagnosticsParams { +// uri: DocumentUri; +// diagnostics: Diagnostic[]; +// } + +// /* 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'] +// }) + +// // register Monaco languages // TODO: JE. I dont understand why I suddenly had to add this when it worked without before. +// monaco.languages.register({ +// id: 'lean4', +// extensions: ['.lean'] +// }) + +// // 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); + +// /** The input field */ +// export function Typewriter({disabled}: {disabled?: boolean}) { +// let { t } = useTranslation() + +// /** Reference to the hidden multi-line editor */ +// const editor = React.useContext(MonacoEditorContext) +// const model = editor?.getModel() +// const uri = model?.uri.toString() + +// const [oneLineEditor, setOneLineEditor] = useState(null) +// const [processing, setProcessing] = useState(false) + +// const {typewriterInput, setTypewriterInput} = React.useContext(PageContext) + +// const inputRef = useRef() + +// // The context storing all information about the current proof +// const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext) + +// const {gameId, worldId, levelId} = React.useContext(GameIdContext) + +// // state to store the last batch of deleted messages +// const {setDeletedChat} = React.useContext(ChatContext) + +// const rpcSess = React.useContext(RpcContext) + +// // Run the command +// const runCommand = React.useCallback(() => { +// if (processing) {return} + +// // TODO: Desired logic is to only reset this after a new *error-free* command has been entered +// setDeletedChat([]) + +// const pos = editor?.getPosition() +// if (typewriterInput) { +// setProcessing(true) +// editor?.executeEdits("typewriter", [{ +// range: monaco.Selection.fromPositions( +// pos, +// editor?.getModel()?.getFullModelRange()?.getEndPosition() +// ), +// text: typewriterInput.trim() + "\n", +// forceMoveMarkers: false +// }]) +// setTypewriterInput('') +// // Load proof after executing edits +// loadGoals(rpcSess, uri, setProof, setCrashed) +// } + +// editor?.setPosition(pos) +// }, [typewriterInput, editor]) + +// useEffect(() => { +// if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) { +// oneLineEditor.setValue(typewriterInput) +// } +// }, [typewriterInput]) + +// /* Load proof on start/switching to typewriter */ +// useEffect(() => { +// setProof(null) +// loadGoals(rpcSess, uri, setProof, setCrashed) +// }, [gameId, worldId, levelId]) + +// /** If the last step has an error, add the command to the typewriter. */ +// useEffect(() => { +// if (lastStepHasErrors(proof)) { +// setTypewriterInput(proof?.steps[proof?.steps.length - 1].command) +// } +// }, [proof]) + +// // React when answer from the server comes back +// useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => { +// if (params.uri == uri) { +// setProcessing(false) + +// console.log('Received lean diagnostics') +// console.log(params.diagnostics) +// setInterimDiags(params.diagnostics) + +// //loadGoals(rpcSess, uri, setProof) + +// // TODO: loadAllGoals() +// if (!hasErrors(params.diagnostics)) { +// //setTypewriterInput("") +// editor?.setPosition(editor?.getModel()?.getFullModelRange()?.getEndPosition()) +// } +// } else { +// // console.debug(`expected uri: ${uri}, got: ${params.uri}`) +// // console.debug(params) +// } +// // 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]); + +// // // React when answer from the server comes back +// // useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => { +// // console.log('Received game diagnostics') +// // console.log(`diag. uri : ${params.uri}`) +// // console.log(params.diagnostics) + +// // }, [uri]); + +// useEffect(() => { +// const myEditor = monaco.editor.create(inputRef.current!, { +// value: typewriterInput, +// language: "lean4cmd", +// quickSuggestions: false, +// lightbulb: { +// enabled: true +// }, +// unicodeHighlight: { +// ambiguousCharacters: false, +// }, +// automaticLayout: true, +// minimap: { +// enabled: false +// }, +// lineNumbers: 'off', +// tabSize: 2, +// glyphMargin: false, +// folding: false, +// lineDecorationsWidth: 0, +// lineNumbersMinChars: 0, +// 'semanticHighlighting.enabled': true, +// overviewRulerLanes: 0, +// hideCursorInOverviewRuler: true, +// scrollbar: { +// vertical: 'hidden', +// horizontalScrollbarSize: 3 +// }, +// overviewRulerBorder: false, +// theme: 'vs-code-theme-converted', +// fontFamily: "JuliaMono", +// contextmenu: false +// }) + +// 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() +// setTypewriterInput(value) +// const newValue = value.replace(/[\n\r]/g, '') +// if (value != newValue) { +// oneLineEditor.setValue(newValue) +// } +// }) +// return () => { l.dispose() } +// }, [oneLineEditor, setTypewriterInput]) + +// useEffect(() => { +// if (!oneLineEditor) return +// // Run command when pressing enter +// const l = oneLineEditor.onKeyUp((ev) => { +// if (ev.code === "Enter" || ev.code === "NumpadEnter") { +// runCommand() +// } +// }) +// return () => { l.dispose() } +// }, [oneLineEditor, runCommand]) + +// // 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) +// // console.debug('LOAD ALL GOALS') +// // TODO: loadAllGoals() +// }, [rpcSess]) + +// /** Process the entered command */ +// const handleSubmit : React.FormEventHandler = (ev) => { +// ev.preventDefault() +// runCommand() +// } + +// // do not display if the proof is completed (with potential warnings still present) +// return
+//
+//
+//
+//
+// +// +//
+// } + +// /** Checks whether the diagnostics contain any errors or warnings to check whether the level has +// been completed.*/ +// export function hasErrors(diags: Diagnostic[]) { +// return diags.some( +// (d) => +// !d.message.startsWith("unsolved goals") && +// (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning +// ) +// } + +// // TODO: Didn't manage to unify this with the one above +// export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) { +// return (typeof diags !== 'undefined') && diags.some( +// (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning +// ) +// } + +// export function getInteractiveDiagsAt (proof: ProofState, k : number) { +// if (k == 0) { +// return [] +// } else if (k >= proof?.steps.length-1) { +// // TODO: Do we need that? +// return proof?.diagnostics.filter(msg => msg.range.start.line >= proof?.steps.length-1) +// } else { +// return proof?.diagnostics.filter(msg => msg.range.start.line == k-1) +// } +// } diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 6593541..52777a0 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -7,17 +7,18 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faHome, faArrowRight, faCode, faTerminal } from '@fortawesome/free-solid-svg-icons' import { CircularProgress } from '@mui/material' import type { Location } from 'vscode-languageserver-protocol' -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider' -import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter' -import { InfoProvider } from 'lean4web/client/src/editor/infoview' -import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter' -import { InfoviewApi } from '@leanprover/infoview' -import { EditorContext } from '../../../node_modules/lean4-infoview/src/infoview/contexts' -import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection' -import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event' -import { Diagnostic } from 'vscode-languageserver-types' -import { DiagnosticSeverity } from 'vscode-languageclient'; +import * as monaco from 'monaco-editor' +// import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' +// import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider' +// import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter' +// import { InfoProvider } from 'lean4web/client/src/editor/infoview' +// import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter' +// import { InfoviewApi } from '@leanprover/infoview' +// import { EditorContext } from '../../../node_modules/lean4-infoview/src/infoview/contexts' +// import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection' +// import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event' +// import { Diagnostic } from 'vscode-languageserver-types' +// import { DiagnosticSeverity } from 'vscode-languageclient'; import { useAppDispatch, useAppSelector } from '../hooks' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api' @@ -25,11 +26,10 @@ import { changedSelection, codeEdited, selectCode, selectSelections, selectCompl selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress' import { store } from '../state/store' import {InventoryPanel} from './inventory' -import { Editor } from './editor' import { Typewriter } from './typewriter' import { ChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, PageContext, GameIdContext } from '../state/context' -import { DualEditor, ExerciseStatement } from './infoview/main' +// import { DualEditor, ExerciseStatement } from './infoview/main' import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api' import path from 'path'; @@ -37,25 +37,92 @@ import '@fontsource/roboto/300.css' import '@fontsource/roboto/400.css' import '@fontsource/roboto/500.css' import '@fontsource/roboto/700.css' -import 'lean4web/client/src/editor/infoview.css' -import 'lean4web/client/src/editor/vscode.css' +// import 'lean4web/client/src/editor/infoview.css' +// import 'lean4web/client/src/editor/vscode.css' import '../css/level.css' -import { LeanClient } from 'lean4web/client/src/editor/leanclient' -import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader' -import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc' -import { IConnectionProvider } from 'monaco-languageclient' -import { monacoSetup } from 'lean4web/client/src/monacoSetup' -import { onigasmH } from 'onigasm/lib/onigasmH' -import { isLastStepWithErrors, lastStepHasErrors } from './infoview/goals' +// import { LeanClient } from 'lean4web/client/src/editor/leanclient' +// import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader' +// import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc' +// import { IConnectionProvider } from 'monaco-languageclient' +// import { monacoSetup } from 'lean4web/client/src/monacoSetup' +// import { onigasmH } from 'onigasm/lib/onigasmH' +// import { isLastStepWithErrors, lastStepHasErrors } from './infoview/goals' import { InfoPopup } from './popup/info' import { PreferencesPopup } from './popup/preferences' import { useTranslation } from 'react-i18next' import i18next from 'i18next' import { ChatButtons } from './chat' import { NavButton } from './navigation' +import { ExerciseStatement } from './editor/ExcerciseStatement' +import { Editor } from './editor/Editor' -monacoSetup() +export function NewLevel({visible = true}) { + const dispatch = useAppDispatch() + let { t } = useTranslation() + const {gameId, worldId, levelId} = React.useContext(GameIdContext) + const { mobile } = useContext(PreferencesContext) + + const [lockEditorMode, setLockEditorMode] = useState(false) + + const gameInfo = useGetGameInfoQuery({game: gameId}) + const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + const typewriterMode = useSelector(selectTypewriterMode(gameId)) + + const proofPanelRef = React.useRef(null) + + const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({ + game: gameId, + typewriterMode: newTypewriterMode + })) + + // Load the namespace of the game + i18next.loadNamespaces(gameId).catch(err => { + console.warn(`translations for ${gameId} do not exist.`) + }) + + /** toggle input mode if allowed */ + function toggleInputMode(ev: React.MouseEvent) { + if (!lockEditorMode) { + setTypewriterMode(!typewriterMode) + console.log('test') + } + } + + return
+ { // Display world image if it exists. + gameInfo.data?.worlds.nodes[worldId].image && +
+ +
+ } + { levelId > 0 && +
+ toggleInputMode(ev)} + title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} /> +
+
+ + + {/*
*/} + {/*
*/} + {/* */} + {/* { typewriterMode ? : } */} +
+
+ } +
+} + + + + +// monacoSetup() export function Level({visible = true}) { let { t } = useTranslation() @@ -114,33 +181,33 @@ export function Level({visible = true}) { } - 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 - }]); - } + // 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 + // }]); + // } // Select and highlight proof steps and corresponding hints // TODO: with the new design, there is no difference between the introduction and @@ -148,62 +215,62 @@ export function Level({visible = true}) { const [selectedStep, setSelectedStep] = useState() - useEffect (() => { - // Lock editor mode - if (levelInfo.data?.template) { - setLockEditorMode(true) - - 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${levelInfo.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: levelInfo.data.template + `\n`, - forceMoveMarkers: true - }]) - } else { - console.debug(`not inserting template.`) - } - } - } else { - setLockEditorMode(false) - } - }, [levelInfo, levelId, worldId, gameId, editor]) - - - useEffect(() => { - // TODO: That's a problem if the saved proof contains an error - // Reset command line input when loading a new level - setTypewriterInput("") - - // Load the selected help steps from the store - setShowHelp(new Set(selectHelp(gameId, worldId, levelId)(store.getState()))) - }, [gameId, worldId, levelId]) - - useEffect(() => { - if (!(typewriterMode && !lockEditorMode) && editor) { - // Delete last input attempt from command line - editor.executeEdits("typewriter", [{ - range: editor.getSelection(), - text: "", - forceMoveMarkers: false - }]); - editor.focus() - } - }, [typewriterMode, lockEditorMode]) + // useEffect (() => { + // // Lock editor mode + // if (levelInfo.data?.template) { + // setLockEditorMode(true) + + // 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${levelInfo.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: levelInfo.data.template + `\n`, + // forceMoveMarkers: true + // }]) + // } else { + // console.debug(`not inserting template.`) + // } + // } + // } else { + // setLockEditorMode(false) + // } + // }, [levelInfo, levelId, worldId, gameId, editor]) + + + // useEffect(() => { + // // TODO: That's a problem if the saved proof contains an error + // // Reset command line input when loading a new level + // setTypewriterInput("") + + // // Load the selected help steps from the store + // setShowHelp(new Set(selectHelp(gameId, worldId, levelId)(store.getState()))) + // }, [gameId, worldId, levelId]) + + // useEffect(() => { + // if (!(typewriterMode && !lockEditorMode) && editor) { + // // Delete last input attempt from command line + // editor.executeEdits("typewriter", [{ + // range: editor.getSelection(), + // text: "", + // forceMoveMarkers: false + // }]); + // editor.focus() + // } + // }, [typewriterMode, lockEditorMode]) useEffect(() => { // Forget whether hidden hints are displayed for steps that don't exist yet @@ -222,14 +289,15 @@ export function Level({visible = true}) { }, [showHelp]) // Effect when command line mode gets enabled - useEffect(() => { - if (onigasmH && editor && (typewriterMode && !lockEditorMode)) { - 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 - }]); + // useEffect(() => { + // if (//onigasmH && + // editor && (typewriterMode && !lockEditorMode)) { + // 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() !== "") { @@ -245,18 +313,18 @@ export function Level({visible = true}) { // // This is not a position that would naturally occur from Typewriter, reset: // editor.setSelection(monaco.Selection.fromPositions(endPos, endPos)) // } - } - }, [editor, typewriterMode, lockEditorMode, onigasmH == null]) + // } + // }, [editor, typewriterMode, lockEditorMode, ])//onigasmH == null]) return
{/*
*/} - - + {/* + */} {levelId > 0 && } - - + {/* + */}
} @@ -286,18 +354,6 @@ export function LevelWrapper({visible = true}) { const lastLevel = levelId >= gameInfo.data?.worldSize[worldId] const { proof } = useContext(ProofContext) - // // impressum pop-up - // function toggleImpressum() {setImpressum(!impressum)} - // function togglePrivacy() {setPrivacy(!privacy)} - - // When clicking on an inventory item, the inventory is overlayed by the item's doc. - // If this state is set to a pair `(name, type)` then the according doc will be open. - // Set `inventoryDoc` to `null` to close the doc - const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null) - function closeInventoryDoc () {setInventoryDoc(null)} - - - const dispatch = useAppDispatch() const typewriterMode = useSelector(selectTypewriterMode(gameId)) @@ -537,7 +593,7 @@ export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.M const gameInfo = useGetGameInfoQuery({game: gameId}) return
- + {/* */}
} @@ -632,170 +688,170 @@ export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.M // // } -function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) { +// function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) { - const {gameId, worldId, levelId} = React.useContext(GameIdContext) +// const {gameId, worldId, levelId} = React.useContext(GameIdContext) - const [editor, setEditor] = useState(null) - const [infoProvider, setInfoProvider] = useState(null) - const [editorConnection, setEditorConnection] = useState(null) +// const [editor, setEditor] = useState(null) +// const [infoProvider, setInfoProvider] = useState(null) +// const [editorConnection, setEditorConnection] = useState(null) - const uriStr = `file:///${worldId}/${levelId}` - const uri = monaco.Uri.parse(uriStr) +// const uriStr = `file:///${worldId}/${levelId}` +// const uri = monaco.Uri.parse(uriStr) - const inventory: Array = useSelector(selectInventory(gameId)) - const difficulty: number = useSelector(selectDifficulty(gameId)) +// const inventory: Array = useSelector(selectInventory(gameId)) +// const difficulty: number = useSelector(selectDifficulty(gameId)) - useEffect(() => { - // monaco.editor.getModels().forEach(model => model.dispose()); +// useEffect(() => { +// // monaco.editor.getModels().forEach(model => model.dispose()); - console.info(`trying to create model: ${gameId} ${worldId} ${levelId} ${uri}`) - const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri) - if (onDidChangeContent) { - model.onDidChangeContent(() => onDidChangeContent(model.getValue())) - } +// console.info(`trying to create model: ${gameId} ${worldId} ${levelId} ${uri}`) +// const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri) +// if (onDidChangeContent) { +// model.onDidChangeContent(() => onDidChangeContent(model.getValue())) +// } - const editor = monaco.editor.create(codeviewRef.current!, { - model, - glyphMargin: true, - quickSuggestions: false, - lineDecorationsWidth: 5, - folding: false, - lineNumbers: 'on', - lightbulb: { - enabled: true - }, - unicodeHighlight: { - ambiguousCharacters: false, - }, - automaticLayout: true, - minimap: { - enabled: false - }, - lineNumbersMinChars: 3, - tabSize: 2, - 'semanticHighlighting.enabled': true, - fontFamily: "JuliaMono", - theme: 'vs-code-theme-converted' - }) - if (onDidChangeSelection) { - editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections())) - } - if (initialSelections) { - console.debug("Initial Selection: ", initialSelections) - // BUG: Somehow I get an `invalid arguments` bug here - // editor.setSelections(initialSelections) - } - setEditor(editor) - const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor) - - const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId - - const connectionProvider : IConnectionProvider = { - get: async () => { - return await new Promise((resolve, reject) => { - console.log(`connecting ${socketUrl}`) - const websocket = new WebSocket(socketUrl) - websocket.addEventListener('error', (ev) => { - reject(ev) - }) - websocket.addEventListener('message', (msg) => { - // console.log(msg.data) - }) - websocket.addEventListener('open', () => { - const socket = toSocket(websocket) - const reader = new DisposingWebSocketMessageReader(socket) - const writer = new WebSocketMessageWriter(socket) - resolve({ - reader, - writer - }) - }) - }) - } - } +// const editor = monaco.editor.create(codeviewRef.current!, { +// model, +// glyphMargin: true, +// quickSuggestions: false, +// lineDecorationsWidth: 5, +// folding: false, +// lineNumbers: 'on', +// lightbulb: { +// enabled: true +// }, +// unicodeHighlight: { +// ambiguousCharacters: false, +// }, +// automaticLayout: true, +// minimap: { +// enabled: false +// }, +// lineNumbersMinChars: 3, +// tabSize: 2, +// 'semanticHighlighting.enabled': true, +// fontFamily: "JuliaMono", +// theme: 'vs-code-theme-converted' +// }) +// if (onDidChangeSelection) { +// editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections())) +// } +// if (initialSelections) { +// console.debug("Initial Selection: ", initialSelections) +// // BUG: Somehow I get an `invalid arguments` bug here +// // editor.setSelections(initialSelections) +// } +// setEditor(editor) +// const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor) + +// const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId + +// const connectionProvider : IConnectionProvider = { +// get: async () => { +// return await new Promise((resolve, reject) => { +// console.log(`connecting ${socketUrl}`) +// const websocket = new WebSocket(socketUrl) +// websocket.addEventListener('error', (ev) => { +// reject(ev) +// }) +// websocket.addEventListener('message', (msg) => { +// // console.log(msg.data) +// }) +// websocket.addEventListener('open', () => { +// const socket = toSocket(websocket) +// const reader = new DisposingWebSocketMessageReader(socket) +// const writer = new WebSocketMessageWriter(socket) +// resolve({ +// reader, +// writer +// }) +// }) +// }) +// } +// } - // Following `vscode-lean4/webview/index.ts` - const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty}) - const infoProvider = new InfoProvider(client) - // const div: HTMLElement = infoviewRef.current! - const imports = { - '@leanprover/infoview': `${window.location.origin}/index.production.min.js`, - 'react': `${window.location.origin}/react.production.min.js`, - 'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`, - 'react-dom': `${window.location.origin}/react-dom.production.min.js`, - 'react-popper': `${window.location.origin}/react-popper.production.min.js` - } - // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi) - setInfoProvider(infoProvider) - - // TODO: it looks like we get errors "File Changed" here. - client.restart("Lean4Game") - - const editorApi = infoProvider.getApi() - - const editorEvents: EditorEvents = { - initialize: new EventEmitter(), - gotServerNotification: new EventEmitter(), - sentClientNotification: new EventEmitter(), - serverRestarted: new EventEmitter(), - serverStopped: new EventEmitter(), - changedCursorLocation: new EventEmitter(), - changedInfoviewConfig: new EventEmitter(), - runTestScript: new EventEmitter(), - requestedAction: new EventEmitter(), - }; - - // Challenge: write a type-correct fn from `Eventify` to `T` without using `any` - const infoviewApi: InfoviewApi = { - initialize: async l => editorEvents.initialize.fire(l), - gotServerNotification: async (method, params) => { - editorEvents.gotServerNotification.fire([method, params]); - }, - sentClientNotification: async (method, params) => { - editorEvents.sentClientNotification.fire([method, params]); - }, - serverRestarted: async r => editorEvents.serverRestarted.fire(r), - serverStopped: async serverStoppedReason => { - editorEvents.serverStopped.fire(serverStoppedReason) - }, - changedCursorLocation: async loc => editorEvents.changedCursorLocation.fire(loc), - changedInfoviewConfig: async conf => editorEvents.changedInfoviewConfig.fire(conf), - requestedAction: async action => editorEvents.requestedAction.fire(action), - // See https://rollupjs.org/guide/en/#avoiding-eval - // eslint-disable-next-line @typescript-eslint/no-implied-eval - runTestScript: async script => new Function(script)(), - getInfoviewHtml: async () => document.body.innerHTML, - }; - - const ec = new EditorConnection(editorApi, editorEvents); - setEditorConnection(ec) - - editorEvents.initialize.on((loc: Location) => ec.events.changedCursorLocation.fire(loc)) - - setEditor(editor) - setInfoProvider(infoProvider) - - infoProvider.openPreview(editor, infoviewApi) - const taskgutter = new LeanTaskGutter(infoProvider.client, editor) - - // TODO: - // setRestart(() => restart) - - return () => { - editor.dispose(); - model.dispose(); - abbrevRewriter.dispose(); - taskgutter.dispose(); - infoProvider.dispose(); - client.dispose(); - } - }, [gameId, worldId, levelId]) +// // Following `vscode-lean4/webview/index.ts` +// const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty}) +// const infoProvider = new InfoProvider(client) +// // const div: HTMLElement = infoviewRef.current! +// const imports = { +// '@leanprover/infoview': `${window.location.origin}/index.production.min.js`, +// 'react': `${window.location.origin}/react.production.min.js`, +// 'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`, +// 'react-dom': `${window.location.origin}/react-dom.production.min.js`, +// 'react-popper': `${window.location.origin}/react-popper.production.min.js` +// } +// // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi) +// setInfoProvider(infoProvider) + +// // TODO: it looks like we get errors "File Changed" here. +// client.restart("Lean4Game") + +// const editorApi = infoProvider.getApi() + +// const editorEvents: EditorEvents = { +// initialize: new EventEmitter(), +// gotServerNotification: new EventEmitter(), +// sentClientNotification: new EventEmitter(), +// serverRestarted: new EventEmitter(), +// serverStopped: new EventEmitter(), +// changedCursorLocation: new EventEmitter(), +// changedInfoviewConfig: new EventEmitter(), +// runTestScript: new EventEmitter(), +// requestedAction: new EventEmitter(), +// }; + +// // Challenge: write a type-correct fn from `Eventify` to `T` without using `any` +// const infoviewApi: InfoviewApi = { +// initialize: async l => editorEvents.initialize.fire(l), +// gotServerNotification: async (method, params) => { +// editorEvents.gotServerNotification.fire([method, params]); +// }, +// sentClientNotification: async (method, params) => { +// editorEvents.sentClientNotification.fire([method, params]); +// }, +// serverRestarted: async r => editorEvents.serverRestarted.fire(r), +// serverStopped: async serverStoppedReason => { +// editorEvents.serverStopped.fire(serverStoppedReason) +// }, +// changedCursorLocation: async loc => editorEvents.changedCursorLocation.fire(loc), +// changedInfoviewConfig: async conf => editorEvents.changedInfoviewConfig.fire(conf), +// requestedAction: async action => editorEvents.requestedAction.fire(action), +// // See https://rollupjs.org/guide/en/#avoiding-eval +// // eslint-disable-next-line @typescript-eslint/no-implied-eval +// runTestScript: async script => new Function(script)(), +// getInfoviewHtml: async () => document.body.innerHTML, +// }; + +// const ec = new EditorConnection(editorApi, editorEvents); +// setEditorConnection(ec) + +// editorEvents.initialize.on((loc: Location) => ec.events.changedCursorLocation.fire(loc)) + +// setEditor(editor) +// setInfoProvider(infoProvider) + +// infoProvider.openPreview(editor, infoviewApi) +// const taskgutter = new LeanTaskGutter(infoProvider.client, editor) + +// // TODO: +// // setRestart(() => restart) + +// return () => { +// editor.dispose(); +// model.dispose(); +// abbrevRewriter.dispose(); +// taskgutter.dispose(); +// infoProvider.dispose(); +// client.dispose(); +// } +// }, [gameId, worldId, levelId]) - const showRestartMessage = () => { - // setRestartMessage(true) - console.log("TODO: SHOW RESTART MESSAGE") - } +// const showRestartMessage = () => { +// // setRestartMessage(true) +// console.log("TODO: SHOW RESTART MESSAGE") +// } - return {editor, infoProvider, editorConnection} -} +// return {editor, infoProvider, editorConnection} +// } diff --git a/client/src/components/message.tsx b/client/src/components/message.tsx index 3883eb0..64b259c 100644 --- a/client/src/components/message.tsx +++ b/client/src/components/message.tsx @@ -5,7 +5,7 @@ import '@fontsource/roboto/500.css'; import '@fontsource/roboto/700.css'; import { Button, Dialog, DialogContent, DialogContentText, DialogActions } from '@mui/material'; -import Markdown from './markdown'; +import { Markdown } from './utils'; function Message({ isOpen, content, close }) { diff --git a/client/src/css/app.css b/client/src/css/app.css index d0d4046..a4b6405 100644 --- a/client/src/css/app.css +++ b/client/src/css/app.css @@ -11,6 +11,10 @@ /* General styling */ +html, body, #root, .app { + height: 100%; +} + body { font-family: "Roboto", sans-serif; -webkit-font-smoothing: antialiased; @@ -92,12 +96,7 @@ em { /* App Bar */ -#root { - height: 100%; -} - .app { - height: 100%; display: flex; flex-direction: column; } diff --git a/client/src/css/editor.css b/client/src/css/editor.css new file mode 100644 index 0000000..6ab0b1e --- /dev/null +++ b/client/src/css/editor.css @@ -0,0 +1,17 @@ +.editor-wrapper { + flex: 1; +} + +#editor { + height: 400px; +} + +#infoview { + height: 400px; +} + +#infoview iframe { + width: 100%; + height: 95%; /* TODO: setting this to 100% makes it a few pixels too high... */ + border: unset; +} diff --git a/client/src/css/game.css b/client/src/css/game.css index 9dc2ee2..7999864 100644 --- a/client/src/css/game.css +++ b/client/src/css/game.css @@ -27,7 +27,6 @@ overflow: auto; position: relative; scroll-behavior: smooth; - } .slider .column { diff --git a/client/src/css/level.css b/client/src/css/level.css index 09e7583..23ddf54 100644 --- a/client/src/css/level.css +++ b/client/src/css/level.css @@ -313,6 +313,8 @@ td code { .editor-mode .proof { height: 100%; + display: flex; + flex-direction: column; } .editor-mode .tmp-pusher {