WIP implementing new editor
Jon Eugster
2 years ago
parent
545ac8b0f7
commit
3a885245ae
@ -1,7 +0,0 @@
|
||||
import * as React from 'react'
|
||||
|
||||
export function Editor () {
|
||||
return <p>
|
||||
I'm an editor
|
||||
</p>
|
||||
}
|
||||
@ -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<HTMLDivElement>(null)
|
||||
const infoviewRef = useRef<HTMLDivElement>(null)
|
||||
const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor>()
|
||||
const [leanMonaco, setLeanMonaco] = useState<LeanMonaco>()
|
||||
const [code, setCode] = useState<string>('')
|
||||
|
||||
const [options, setOptions] = useState<LeanMonacoOptions>({
|
||||
// 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 <Split direction='vertical' minSize={200} sizes={[50, 50]}
|
||||
className={`editor-wrapper ${typewriterMode ? 'hidden' : ''}`} >
|
||||
<div ref={editorRef} id="editor" />
|
||||
<div ref={infoviewRef} id="infoview" />
|
||||
</Split>
|
||||
}
|
||||
@ -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 <>
|
||||
<div className="exercise-statement">
|
||||
{levelInfo.data?.descrText ?
|
||||
<Markdown>
|
||||
{(levelInfo.data?.displayName ? `**${t("Theorem")}** \`${levelInfo.data?.displayName}\`: ` : '') + t(levelInfo.data?.descrText, {ns: gameId})}
|
||||
</Markdown> : levelInfo.data?.displayName &&
|
||||
<Markdown>
|
||||
{`**${t("Theorem")}** \`${levelInfo.data?.displayName}\``}
|
||||
</Markdown>
|
||||
}
|
||||
{levelInfo.data?.descrFormat && showLeanStatement &&
|
||||
<p><code className="lean-code">{levelInfo.data?.descrFormat}</code></p>
|
||||
}
|
||||
</div>
|
||||
</>
|
||||
}
|
||||
@ -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) =>
|
||||
<span className={namecls + (isInaccessibleName(n) ? 'goal-inaccessible ' : '')} key={i}>
|
||||
<SelectableLocation
|
||||
locs={locs}
|
||||
loc={mvarId && h.fvarIds && h.fvarIds.length > i ?
|
||||
{ mvarId, loc: { hyp: h.fvarIds[i] }} :
|
||||
undefined
|
||||
}
|
||||
alwaysHighlight={false}
|
||||
>{n}</SelectableLocation>
|
||||
</span>)
|
||||
|
||||
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 <div>
|
||||
<strong className="goal-hyp">{names}</strong>
|
||||
:
|
||||
<LocationsContext.Provider value={typeLocs}>
|
||||
<InteractiveCode fmt={h.type} />
|
||||
</LocationsContext.Provider>
|
||||
{h.val &&
|
||||
<LocationsContext.Provider value={valLocs}>
|
||||
:= <InteractiveCode fmt={h.val} />
|
||||
</LocationsContext.Provider>}
|
||||
</div>
|
||||
}
|
||||
|
||||
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 = <div key={'goal'} className="goal">
|
||||
{/* <div className="goal-title">{t("Goal")}:</div> */}
|
||||
<LocationsContext.Provider value={goalLocs}>
|
||||
<InteractiveCode fmt={goal.type} />
|
||||
</LocationsContext.Provider>
|
||||
</div>
|
||||
|
||||
// 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 = <Hints hints={goal.hints} key={goal.mvarId} />
|
||||
const objectHyps = unbundleHyps(hyps.filter(hyp => !hyp.isAssumption))
|
||||
const assumptionHyps = unbundleHyps(hyps.filter(hyp => hyp.isAssumption))
|
||||
|
||||
return <>
|
||||
{/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
|
||||
{filter.reverse && goalLi}
|
||||
<div className="hypotheses">
|
||||
{! typewriter && objectHyps.length > 0 &&
|
||||
<div className="hyp-group"><div className="hyp-group-title">{t("Objects")}:</div>
|
||||
{objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
|
||||
{!typewriter && assumptionHyps.length > 0 &&
|
||||
<div className="hyp-group"><div className="hyp-group-title">{t("Assumptions")}:</div>
|
||||
{assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
|
||||
</div>
|
||||
{!filter.reverse && <>
|
||||
<div className='goal-sign'>
|
||||
<svg width="100%" height="100%">
|
||||
<line x1="0%" y1="0%" x2="0%" y2="100%" />
|
||||
<line x1="0%" y1="50%" x2="100%" y2="50%" />
|
||||
</svg>
|
||||
</div>
|
||||
{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 = <div key={'goal'}>
|
||||
<div className="goal-title">{t("Goal") + ":"}</div>
|
||||
<LocationsContext.Provider value={goalLocs}>
|
||||
<InteractiveCode fmt={goal.type} />
|
||||
</LocationsContext.Provider>
|
||||
</div>
|
||||
|
||||
const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
|
||||
const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
|
||||
|
||||
return <div id="main-assumptions">
|
||||
<div className="goals-section-title">{t("Current Goal")}</div>
|
||||
{filter.reverse && goalLi}
|
||||
{ objectHyps.length > 0 &&
|
||||
<div className="hyp-group"><div className="hyp-group-title">{t("Objects") + ":"}</div>
|
||||
{objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
|
||||
{ assumptionHyps.length > 0 &&
|
||||
<div className="hyp-group">
|
||||
<div className="hyp-group-title">{t("Assumptions") + ":"}</div>
|
||||
{assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
|
||||
</div> }
|
||||
</div>
|
||||
})
|
||||
|
||||
export const OtherGoals = React.memo((props: GoalProps2) => {
|
||||
let { t } = useTranslation()
|
||||
const { goals, filter } = props
|
||||
return <>
|
||||
{goals && goals.length > 1 &&
|
||||
<div id="other-goals" className="other-goals">
|
||||
<div className="goals-section-title">{t("Further Goals")}</div>
|
||||
{goals.slice(1).map((goal, i) =>
|
||||
<details key={i}>
|
||||
<summary>
|
||||
<InteractiveCode fmt={goal.type} />
|
||||
</summary>
|
||||
<Goal typewriter={false} filter={filter} goal={goal} />
|
||||
</details>)}
|
||||
</div>}
|
||||
</>
|
||||
})
|
||||
|
||||
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) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}
|
||||
</>
|
||||
}
|
||||
}
|
||||
|
||||
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 =
|
||||
<a className="link pointer mh2 dim codicon codicon-quote"
|
||||
data-id="copy-goal-to-comment"
|
||||
onClick={e => {
|
||||
e.preventDefault();
|
||||
if (goals) void ec.copyToComment(goalsWithHintsToString(goals))
|
||||
}}
|
||||
title="copy state to comment" />
|
||||
|
||||
const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>(
|
||||
{ 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 =
|
||||
<a className={sortClasses} title="reverse list"
|
||||
onClick={_ => setGoalFilters(s => ({ ...s, reverse: !s.reverse }))} />
|
||||
|
||||
const mkFilterButton = (filterFn: React.SetStateAction<GoalFilterState>, filledFn: (_: GoalFilterState) => boolean, name: string) =>
|
||||
<a className='link pointer tooltip-menu-content' onClick={_ => { setGoalFilters(filterFn) }}>
|
||||
<span className={'tooltip-menu-icon codicon ' + (filledFn(goalFilters) ? 'codicon-check ' : 'codicon-blank ')}> </span>
|
||||
<span className='tooltip-menu-text '>{name}</span>
|
||||
</a>
|
||||
const filterMenu = <span>
|
||||
{mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')}
|
||||
<br/>
|
||||
{mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')}
|
||||
<br/>
|
||||
{mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')}
|
||||
<br/>
|
||||
{mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')}
|
||||
</span>
|
||||
|
||||
const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue
|
||||
const filterButton =
|
||||
<WithTooltipOnHover mkTooltipContent={() => filterMenu}>
|
||||
<a className={'link pointer mh2 dim codicon ' + (isFiltered ? 'codicon-filter-filled ': 'codicon-filter ')}/>
|
||||
</WithTooltipOnHover>
|
||||
|
||||
return <div style={{display: goals !== undefined ? 'block' : 'none'}}>
|
||||
<details open>
|
||||
<summary className='mv2 pointer'>
|
||||
{headerChildren}
|
||||
<span className='fr'>{copyToCommentButton}{sortButton}{filterButton}</span>
|
||||
</summary>
|
||||
<div className='ml1'>
|
||||
{goals && <Goals goals={goals} filter={goalFilters}></Goals>}
|
||||
</div>
|
||||
</details>
|
||||
</div>
|
||||
})
|
||||
|
||||
export function loadGoals(
|
||||
rpcSess: RpcSessionAtPos,
|
||||
uri: string,
|
||||
setProof: React.Dispatch<React.SetStateAction<ProofState>>,
|
||||
setCrashed: React.Dispatch<React.SetStateAction<Boolean>>) {
|
||||
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) =>
|
||||
// <span className={namecls + (isInaccessibleName(n) ? 'goal-inaccessible ' : '')} key={i}>
|
||||
// <SelectableLocation
|
||||
// locs={locs}
|
||||
// loc={mvarId && h.fvarIds && h.fvarIds.length > i ?
|
||||
// { mvarId, loc: { hyp: h.fvarIds[i] }} :
|
||||
// undefined
|
||||
// }
|
||||
// alwaysHighlight={false}
|
||||
// >{n}</SelectableLocation>
|
||||
// </span>)
|
||||
|
||||
// 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 <div>
|
||||
// <strong className="goal-hyp">{names}</strong>
|
||||
// :
|
||||
// <LocationsContext.Provider value={typeLocs}>
|
||||
// <InteractiveCode fmt={h.type} />
|
||||
// </LocationsContext.Provider>
|
||||
// {h.val &&
|
||||
// <LocationsContext.Provider value={valLocs}>
|
||||
// := <InteractiveCode fmt={h.val} />
|
||||
// </LocationsContext.Provider>}
|
||||
// </div>
|
||||
// }
|
||||
|
||||
// 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 = <div key={'goal'} className="goal">
|
||||
// {/* <div className="goal-title">{t("Goal")}:</div> */}
|
||||
// <LocationsContext.Provider value={goalLocs}>
|
||||
// <InteractiveCode fmt={goal.type} />
|
||||
// </LocationsContext.Provider>
|
||||
// </div>
|
||||
|
||||
// // 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 = <Hints hints={goal.hints} key={goal.mvarId} />
|
||||
// const objectHyps = unbundleHyps(hyps.filter(hyp => !hyp.isAssumption))
|
||||
// const assumptionHyps = unbundleHyps(hyps.filter(hyp => hyp.isAssumption))
|
||||
|
||||
// return <>
|
||||
// {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
|
||||
// {filter.reverse && goalLi}
|
||||
// <div className="hypotheses">
|
||||
// {! typewriter && objectHyps.length > 0 &&
|
||||
// <div className="hyp-group"><div className="hyp-group-title">{t("Objects")}:</div>
|
||||
// {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
|
||||
// {!typewriter && assumptionHyps.length > 0 &&
|
||||
// <div className="hyp-group"><div className="hyp-group-title">{t("Assumptions")}:</div>
|
||||
// {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
|
||||
// </div>
|
||||
// {!filter.reverse && <>
|
||||
// <div className='goal-sign'>
|
||||
// <svg width="100%" height="100%">
|
||||
// <line x1="0%" y1="0%" x2="0%" y2="100%" />
|
||||
// <line x1="0%" y1="50%" x2="100%" y2="50%" />
|
||||
// </svg>
|
||||
// </div>
|
||||
// {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 = <div key={'goal'}>
|
||||
// <div className="goal-title">{t("Goal") + ":"}</div>
|
||||
// <LocationsContext.Provider value={goalLocs}>
|
||||
// <InteractiveCode fmt={goal.type} />
|
||||
// </LocationsContext.Provider>
|
||||
// </div>
|
||||
|
||||
// const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
|
||||
// const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
|
||||
|
||||
// return <div id="main-assumptions">
|
||||
// <div className="goals-section-title">{t("Current Goal")}</div>
|
||||
// {filter.reverse && goalLi}
|
||||
// { objectHyps.length > 0 &&
|
||||
// <div className="hyp-group"><div className="hyp-group-title">{t("Objects") + ":"}</div>
|
||||
// {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
|
||||
// { assumptionHyps.length > 0 &&
|
||||
// <div className="hyp-group">
|
||||
// <div className="hyp-group-title">{t("Assumptions") + ":"}</div>
|
||||
// {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
|
||||
// </div> }
|
||||
// </div>
|
||||
// })
|
||||
|
||||
// export const OtherGoals = React.memo((props: GoalProps2) => {
|
||||
// let { t } = useTranslation()
|
||||
// const { goals, filter } = props
|
||||
// return <>
|
||||
// {goals && goals.length > 1 &&
|
||||
// <div id="other-goals" className="other-goals">
|
||||
// <div className="goals-section-title">{t("Further Goals")}</div>
|
||||
// {goals.slice(1).map((goal, i) =>
|
||||
// <details key={i}>
|
||||
// <summary>
|
||||
// <InteractiveCode fmt={goal.type} />
|
||||
// </summary>
|
||||
// <Goal typewriter={false} filter={filter} goal={goal} />
|
||||
// </details>)}
|
||||
// </div>}
|
||||
// </>
|
||||
// })
|
||||
|
||||
// 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) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}
|
||||
// </>
|
||||
// }
|
||||
// }
|
||||
|
||||
// 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 =
|
||||
// <a className="link pointer mh2 dim codicon codicon-quote"
|
||||
// data-id="copy-goal-to-comment"
|
||||
// onClick={e => {
|
||||
// e.preventDefault();
|
||||
// if (goals) void ec.copyToComment(goalsWithHintsToString(goals))
|
||||
// }}
|
||||
// title="copy state to comment" />
|
||||
|
||||
// const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>(
|
||||
// { 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 =
|
||||
// <a className={sortClasses} title="reverse list"
|
||||
// onClick={_ => setGoalFilters(s => ({ ...s, reverse: !s.reverse }))} />
|
||||
|
||||
// const mkFilterButton = (filterFn: React.SetStateAction<GoalFilterState>, filledFn: (_: GoalFilterState) => boolean, name: string) =>
|
||||
// <a className='link pointer tooltip-menu-content' onClick={_ => { setGoalFilters(filterFn) }}>
|
||||
// <span className={'tooltip-menu-icon codicon ' + (filledFn(goalFilters) ? 'codicon-check ' : 'codicon-blank ')}> </span>
|
||||
// <span className='tooltip-menu-text '>{name}</span>
|
||||
// </a>
|
||||
// const filterMenu = <span>
|
||||
// {mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')}
|
||||
// <br/>
|
||||
// {mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')}
|
||||
// <br/>
|
||||
// {mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')}
|
||||
// <br/>
|
||||
// {mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')}
|
||||
// </span>
|
||||
|
||||
// const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue
|
||||
// const filterButton =
|
||||
// <WithTooltipOnHover mkTooltipContent={() => filterMenu}>
|
||||
// <a className={'link pointer mh2 dim codicon ' + (isFiltered ? 'codicon-filter-filled ': 'codicon-filter ')}/>
|
||||
// </WithTooltipOnHover>
|
||||
|
||||
// return <div style={{display: goals !== undefined ? 'block' : 'none'}}>
|
||||
// <details open>
|
||||
// <summary className='mv2 pointer'>
|
||||
// {headerChildren}
|
||||
// <span className='fr'>{copyToCommentButton}{sortButton}{filterButton}</span>
|
||||
// </summary>
|
||||
// <div className='ml1'>
|
||||
// {goals && <Goals goals={goals} filter={goalFilters}></Goals>}
|
||||
// </div>
|
||||
// </details>
|
||||
// </div>
|
||||
// })
|
||||
|
||||
// export function loadGoals(
|
||||
// rpcSess: RpcSessionAtPos,
|
||||
// uri: string,
|
||||
// setProof: React.Dispatch<React.SetStateAction<ProofState>>,
|
||||
// setCrashed: React.Dispatch<React.SetStateAction<Boolean>>) {
|
||||
// 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)
|
||||
// }
|
||||
|
||||
@ -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<void>
|
||||
}
|
||||
|
||||
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 (
|
||||
<summary style={{transition: 'color 0.5s ease'}} className={'mv2 pointer ' + statusColor}>
|
||||
{locationString}
|
||||
{isPinned && !isPaused && ' (pinned)'}
|
||||
{!isPinned && isPaused && ' (paused)'}
|
||||
{isPinned && isPaused && ' (pinned and paused)'}
|
||||
<span className='fr'>
|
||||
{isPinned &&
|
||||
<a className='link pointer mh2 dim codicon codicon-go-to-file'
|
||||
data-id='reveal-file-location'
|
||||
onClick={e => { e.preventDefault(); void ec.revealPosition(pos); }}
|
||||
title='reveal file location' />}
|
||||
<a className={'link pointer mh2 dim codicon ' + (isPinned ? 'codicon-pinned ' : 'codicon-pin ')}
|
||||
data-id='toggle-pinned'
|
||||
onClick={e => { e.preventDefault(); onPin(pos); }}
|
||||
title={isPinned ? 'unpin' : 'pin'} />
|
||||
<a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue ' : 'codicon-debug-pause ')}
|
||||
data-id='toggle-paused'
|
||||
onClick={e => { e.preventDefault(); setPaused(!isPaused) }}
|
||||
title={isPaused ? 'continue updating' : 'pause updating'} />
|
||||
<a className='link pointer mh2 dim codicon codicon-refresh'
|
||||
data-id='update'
|
||||
onClick={e => { e.preventDefault(); void triggerUpdate() }}
|
||||
title='update'/>
|
||||
</span>
|
||||
</summary>
|
||||
)
|
||||
})
|
||||
|
||||
interface InfoDisplayContentProps extends PausableProps {
|
||||
pos: DocumentPosition
|
||||
messages: InteractiveDiagnostic[]
|
||||
goals?: InteractiveGoals
|
||||
termGoal?: InteractiveTermGoal
|
||||
error?: string
|
||||
userWidgets: UserWidgetInstance[]
|
||||
triggerUpdate: () => Promise<void>
|
||||
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<GoalsLocation[]>([])
|
||||
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 &&
|
||||
<div className='error' key='errors'>
|
||||
Error updating:{' '}{error}.
|
||||
<a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>{' '}Try again.</a>
|
||||
</div>}
|
||||
<AllMessages /> {/* TODO: Move error messages to Chat instead */}
|
||||
<LocationsContext.Provider value={locs}>
|
||||
<div className="goals-section">
|
||||
|
||||
{ goals && goals.goals.length > 0 && <>
|
||||
<GoalsTabs goals={goals.goals.map(goal => ({goal: goal, hints: []}))} last={false} onClick={() => {}} onGoalChange={() => {}}/>
|
||||
{/* <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
|
||||
<OtherGoals filter={goalFilter} goals={goals.goals} /> */}
|
||||
</>}
|
||||
</div>
|
||||
{/* <div>
|
||||
{ goals && (goals.goals.length > 0
|
||||
? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
|
||||
: <div className="goals-section-title">{t("No Goals")}</div>
|
||||
)}
|
||||
</div> */}
|
||||
</LocationsContext.Provider>
|
||||
{/* {userWidgets.map(widget =>
|
||||
<details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
|
||||
<summary className='mv2 pointer'>{widget.name}</summary>
|
||||
<PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []}
|
||||
termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
|
||||
</details>
|
||||
)} */}
|
||||
{/* {nothingToShow && (
|
||||
isPaused ?
|
||||
/* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 * /
|
||||
<span>Updating is paused.{' '}
|
||||
<a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>Refresh</a>
|
||||
{' '}or <a className='link pointer dim' onClick={e => { e.preventDefault(); setPaused(false) }}>resume updating</a>
|
||||
{' '}to see information.
|
||||
</span> :
|
||||
<><CircularProgress /><div>{t("Loading goal…")}</div></>)} */}
|
||||
{/* <LocationsContext.Provider value={locs}>
|
||||
{goals && goals.goals.length > 1 && <div className="goals-section other-goals">
|
||||
<div className="goals-section-title">Weitere Goals</div>
|
||||
|
||||
{goals.goals.slice(1).map((goal, i) =>
|
||||
<details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal typewriter={false} filter={goalFilter} goal={goal} /></details>)}
|
||||
</div>}
|
||||
</LocationsContext.Provider> */}
|
||||
</>
|
||||
})
|
||||
|
||||
interface InfoDisplayProps {
|
||||
pos: DocumentPosition,
|
||||
status: InfoStatus,
|
||||
messages: InteractiveDiagnostic[],
|
||||
proof?: ProofState,
|
||||
goals?: InteractiveGoals,
|
||||
termGoal?: InteractiveTermGoal,
|
||||
error?: string,
|
||||
userWidgets: UserWidgetInstance[],
|
||||
rpcSess: RpcSessionAtPos,
|
||||
triggerUpdate: () => Promise<void>,
|
||||
}
|
||||
|
||||
/** 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<boolean>(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 (
|
||||
<RpcContext.Provider value={rpcSess}>
|
||||
{/* <details open> */}
|
||||
{/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */}
|
||||
<div className="vscode-light">
|
||||
<InfoDisplayContent {...props} proofString={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
|
||||
</div>
|
||||
{/* </details> */}
|
||||
</RpcContext.Provider>
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 <InfoAtCursor {...props} />
|
||||
else return <InfoAux {...props} pos={props.pos} />
|
||||
}
|
||||
|
||||
function InfoAtCursor(props: InfoProps) {
|
||||
const ec = React.useContext(EditorContext)
|
||||
// eslint-disable-next-line @typescript-eslint/no-non-null-assertion
|
||||
const [curLoc, setCurLoc] = React.useState<Location>(ec.events.changedCursorLocation.current!)
|
||||
useEvent(ec.events.changedCursorLocation, loc => loc && setCurLoc(loc), [])
|
||||
const pos = { uri: curLoc.uri, ...curLoc.range.start }
|
||||
return <InfoAux {...props} pos={pos} />
|
||||
}
|
||||
|
||||
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<Diagnostic[]>([])
|
||||
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<number>(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<InfoDisplayProps, 'triggerUpdate'>
|
||||
const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((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<number>()
|
||||
const clearUpdaterTimeout = () => {
|
||||
if (updaterTimeout.current) {
|
||||
window.clearTimeout(updaterTimeout.current)
|
||||
updaterTimeout.current = undefined
|
||||
}
|
||||
}
|
||||
const triggerUpdate = React.useCallback(() => new Promise<void>(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<InfoDisplayProps>({
|
||||
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 <InfoDisplay kind={props.kind} onPin={props.onPin} {...displayProps} />
|
||||
}
|
||||
// /* 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<void>
|
||||
// }
|
||||
|
||||
// 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 (
|
||||
// <summary style={{transition: 'color 0.5s ease'}} className={'mv2 pointer ' + statusColor}>
|
||||
// {locationString}
|
||||
// {isPinned && !isPaused && ' (pinned)'}
|
||||
// {!isPinned && isPaused && ' (paused)'}
|
||||
// {isPinned && isPaused && ' (pinned and paused)'}
|
||||
// <span className='fr'>
|
||||
// {isPinned &&
|
||||
// <a className='link pointer mh2 dim codicon codicon-go-to-file'
|
||||
// data-id='reveal-file-location'
|
||||
// onClick={e => { e.preventDefault(); void ec.revealPosition(pos); }}
|
||||
// title='reveal file location' />}
|
||||
// <a className={'link pointer mh2 dim codicon ' + (isPinned ? 'codicon-pinned ' : 'codicon-pin ')}
|
||||
// data-id='toggle-pinned'
|
||||
// onClick={e => { e.preventDefault(); onPin(pos); }}
|
||||
// title={isPinned ? 'unpin' : 'pin'} />
|
||||
// <a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue ' : 'codicon-debug-pause ')}
|
||||
// data-id='toggle-paused'
|
||||
// onClick={e => { e.preventDefault(); setPaused(!isPaused) }}
|
||||
// title={isPaused ? 'continue updating' : 'pause updating'} />
|
||||
// <a className='link pointer mh2 dim codicon codicon-refresh'
|
||||
// data-id='update'
|
||||
// onClick={e => { e.preventDefault(); void triggerUpdate() }}
|
||||
// title='update'/>
|
||||
// </span>
|
||||
// </summary>
|
||||
// )
|
||||
// })
|
||||
|
||||
// interface InfoDisplayContentProps extends PausableProps {
|
||||
// pos: DocumentPosition
|
||||
// messages: InteractiveDiagnostic[]
|
||||
// goals?: InteractiveGoals
|
||||
// termGoal?: InteractiveTermGoal
|
||||
// error?: string
|
||||
// userWidgets: UserWidgetInstance[]
|
||||
// triggerUpdate: () => Promise<void>
|
||||
// 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<GoalsLocation[]>([])
|
||||
// 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 &&
|
||||
// <div className='error' key='errors'>
|
||||
// Error updating:{' '}{error}.
|
||||
// <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>{' '}Try again.</a>
|
||||
// </div>}
|
||||
// <AllMessages /> {/* TODO: Move error messages to Chat instead */}
|
||||
// <LocationsContext.Provider value={locs}>
|
||||
// <div className="goals-section">
|
||||
|
||||
// { goals && goals.goals.length > 0 && <>
|
||||
// <GoalsTabs goals={goals.goals.map(goal => ({goal: goal, hints: []}))} last={false} onClick={() => {}} onGoalChange={() => {}}/>
|
||||
// {/* <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
|
||||
// <OtherGoals filter={goalFilter} goals={goals.goals} /> */}
|
||||
// </>}
|
||||
// </div>
|
||||
// {/* <div>
|
||||
// { goals && (goals.goals.length > 0
|
||||
// ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
|
||||
// : <div className="goals-section-title">{t("No Goals")}</div>
|
||||
// )}
|
||||
// </div> */}
|
||||
// </LocationsContext.Provider>
|
||||
// {/* {userWidgets.map(widget =>
|
||||
// <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
|
||||
// <summary className='mv2 pointer'>{widget.name}</summary>
|
||||
// <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []}
|
||||
// termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
|
||||
// </details>
|
||||
// )} */}
|
||||
// {/* {nothingToShow && (
|
||||
// isPaused ?
|
||||
// /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 * /
|
||||
// <span>Updating is paused.{' '}
|
||||
// <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>Refresh</a>
|
||||
// {' '}or <a className='link pointer dim' onClick={e => { e.preventDefault(); setPaused(false) }}>resume updating</a>
|
||||
// {' '}to see information.
|
||||
// </span> :
|
||||
// <><CircularProgress /><div>{t("Loading goal…")}</div></>)} */}
|
||||
// {/* <LocationsContext.Provider value={locs}>
|
||||
// {goals && goals.goals.length > 1 && <div className="goals-section other-goals">
|
||||
// <div className="goals-section-title">Weitere Goals</div>
|
||||
|
||||
// {goals.goals.slice(1).map((goal, i) =>
|
||||
// <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal typewriter={false} filter={goalFilter} goal={goal} /></details>)}
|
||||
// </div>}
|
||||
// </LocationsContext.Provider> */}
|
||||
// </>
|
||||
// })
|
||||
|
||||
// interface InfoDisplayProps {
|
||||
// pos: DocumentPosition,
|
||||
// status: InfoStatus,
|
||||
// messages: InteractiveDiagnostic[],
|
||||
// proof?: ProofState,
|
||||
// goals?: InteractiveGoals,
|
||||
// termGoal?: InteractiveTermGoal,
|
||||
// error?: string,
|
||||
// userWidgets: UserWidgetInstance[],
|
||||
// rpcSess: RpcSessionAtPos,
|
||||
// triggerUpdate: () => Promise<void>,
|
||||
// }
|
||||
|
||||
// /** 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<boolean>(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 (
|
||||
// <RpcContext.Provider value={rpcSess}>
|
||||
// {/* <details open> */}
|
||||
// {/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */}
|
||||
// <div className="vscode-light">
|
||||
// <InfoDisplayContent {...props} proofString={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
|
||||
// </div>
|
||||
// {/* </details> */}
|
||||
// </RpcContext.Provider>
|
||||
// )
|
||||
// }
|
||||
|
||||
// /**
|
||||
// * 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 <InfoAtCursor {...props} />
|
||||
// else return <InfoAux {...props} pos={props.pos} />
|
||||
// }
|
||||
|
||||
// function InfoAtCursor(props: InfoProps) {
|
||||
// const ec = React.useContext(EditorContext)
|
||||
// // eslint-disable-next-line @typescript-eslint/no-non-null-assertion
|
||||
// const [curLoc, setCurLoc] = React.useState<Location>(ec.events.changedCursorLocation.current!)
|
||||
// useEvent(ec.events.changedCursorLocation, loc => loc && setCurLoc(loc), [])
|
||||
// const pos = { uri: curLoc.uri, ...curLoc.range.start }
|
||||
// return <InfoAux {...props} pos={pos} />
|
||||
// }
|
||||
|
||||
// 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<Diagnostic[]>([])
|
||||
// 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<number>(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<InfoDisplayProps, 'triggerUpdate'>
|
||||
// const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((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<number>()
|
||||
// const clearUpdaterTimeout = () => {
|
||||
// if (updaterTimeout.current) {
|
||||
// window.clearTimeout(updaterTimeout.current)
|
||||
// updaterTimeout.current = undefined
|
||||
// }
|
||||
// }
|
||||
// const triggerUpdate = React.useCallback(() => new Promise<void>(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<InfoDisplayProps>({
|
||||
// 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 <InfoDisplay kind={props.kind} onPin={props.onPin} {...displayProps} />
|
||||
// }
|
||||
|
||||
@ -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<Keyed<DocumentPosition>>(),
|
||||
(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<DocumentPosition> = { ...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<DocumentPosition>[];
|
||||
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<number>(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<InfoProps>[] = pinnedPositions.map(pos => ({ kind: 'pin', onPin: unpin, pos, key: pos.key }));
|
||||
if (curPos) infoProps.push({ kind: 'cursor', onPin: pin, key: 'cursor' });
|
||||
|
||||
return <div>
|
||||
{infoProps.map (ps => <Info {...ps} />)}
|
||||
{!curPos && <p>{t("Click somewhere in the Lean file to enable the infoview.")}</p> }
|
||||
</div>;
|
||||
}
|
||||
// /* 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<Keyed<DocumentPosition>>(),
|
||||
// (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<DocumentPosition> = { ...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<DocumentPosition>[];
|
||||
// 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<number>(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<InfoProps>[] = pinnedPositions.map(pos => ({ kind: 'pin', onPin: unpin, pos, key: pos.key }));
|
||||
// if (curPos) infoProps.push({ kind: 'cursor', onPin: pin, key: 'cursor' });
|
||||
|
||||
// return <div>
|
||||
// {infoProps.map (ps => <Info {...ps} />)}
|
||||
// {!curPos && <p>{t("Click somewhere in the Lean file to enable the infoview.")}</p> }
|
||||
// </div>;
|
||||
// }
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@ -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 <div className={severityClass + ' ml1 message'}>
|
||||
{!typewriterMode && <p className="mv2">{title}</p>}
|
||||
<pre className="font-code pre-wrap">
|
||||
<InteractiveMessage fmt={message} />
|
||||
</pre>
|
||||
</div>
|
||||
}
|
||||
|
||||
// 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 <div>
|
||||
{errors.map((err, i) => (<Error key={`error-${i}`} error={err} typewriterMode={typewriterMode}/>))}
|
||||
</div>
|
||||
}
|
||||
|
||||
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 (
|
||||
// <details open>
|
||||
// <summary className={severityClass + ' mv2 pointer'}>{title}
|
||||
// <span className="fr">
|
||||
// <a className="link pointer mh2 dim codicon codicon-go-to-file"
|
||||
// onClick={e => { e.preventDefault(); void ec.revealLocation(loc); }}
|
||||
// title="reveal file location"></a>
|
||||
// <a className="link pointer mh2 dim codicon codicon-quote"
|
||||
// data-id="copy-to-comment"
|
||||
// onClick={e => {e.preventDefault(); void ec.copyToComment(text)}}
|
||||
// title="copy message to comment"></a>
|
||||
// <a className="link pointer mh2 dim codicon codicon-clippy"
|
||||
// onClick={e => {e.preventDefault(); void ec.api.copyToClipboard(text)}}
|
||||
// title="copy message to clipboard"></a>
|
||||
// </span>
|
||||
// </summary>
|
||||
<div className={severityClass + ' ml1 message'}>
|
||||
{!(typewriterMode && !lockEditorMode) && <p className="mv2">{title}</p>}
|
||||
<pre className="font-code pre-wrap">
|
||||
<InteractiveMessage fmt={message} />
|
||||
</pre>
|
||||
</div>
|
||||
// </details>
|
||||
)
|
||||
}, 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 (
|
||||
<div>
|
||||
{mkMessageViewProps(uri, messages).map(m => <MessageView {...m} />)}
|
||||
</div>
|
||||
);
|
||||
})
|
||||
|
||||
function lazy<T>(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<React.Dispatch<React.SetStateAction<boolean>>>();
|
||||
useEvent(ec.events.requestedAction, act => {
|
||||
if (act.kind === 'toggleAllMessages' && setOpenRef.current !== undefined) {
|
||||
setOpenRef.current(t => !t);
|
||||
}
|
||||
});
|
||||
|
||||
return (
|
||||
<RpcContext.Provider value={rs}>
|
||||
{/* <Details setOpenRef={setOpenRef as any} initiallyOpen={!config.autoOpenShowsGoal}>
|
||||
<summary className="mv2 pointer">
|
||||
All Messages ({diags.length})
|
||||
<span className="fr">
|
||||
<a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue' : 'codicon-debug-pause')}
|
||||
onClick={e => { e.preventDefault(); setPaused(p => !p); }}
|
||||
title={isPaused ? 'continue updating' : 'pause updating'}>
|
||||
</a>
|
||||
</span>
|
||||
</summary> */}
|
||||
<AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} curPos={curPos} />
|
||||
{/* </Details> */}
|
||||
</RpcContext.Provider>
|
||||
)
|
||||
}
|
||||
|
||||
/** 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<InteractiveDiagnostic[]>}) {
|
||||
let { t } = useTranslation()
|
||||
const [msgs, setMsgs] = React.useState<InteractiveDiagnostic[] | undefined>(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 <div>{t("Loading messages…")}</div>
|
||||
else return <MessagesList uri={uri} messages={msgs}/>
|
||||
}
|
||||
|
||||
/**
|
||||
* 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<DocumentUri, Diagnostic[]>(),
|
||||
async (params: PublishDiagnosticsParams) => diags =>
|
||||
new Map(diags).set(params.uri, params.diagnostics),
|
||||
[]
|
||||
)
|
||||
|
||||
return <LspDiagnosticsContext.Provider value={allDiags}>{children}</LspDiagnosticsContext.Provider>
|
||||
}
|
||||
|
||||
/** 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 <div className={severityClass + ' ml1 message'}>
|
||||
// {!typewriterMode && <p className="mv2">{title}</p>}
|
||||
// <pre className="font-code pre-wrap">
|
||||
// <InteractiveMessage fmt={message} />
|
||||
// </pre>
|
||||
// </div>
|
||||
// }
|
||||
|
||||
// // 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 <div>
|
||||
// {errors.map((err, i) => (<Error key={`error-${i}`} error={err} typewriterMode={typewriterMode}/>))}
|
||||
// </div>
|
||||
// }
|
||||
|
||||
// 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 (
|
||||
// // <details open>
|
||||
// // <summary className={severityClass + ' mv2 pointer'}>{title}
|
||||
// // <span className="fr">
|
||||
// // <a className="link pointer mh2 dim codicon codicon-go-to-file"
|
||||
// // onClick={e => { e.preventDefault(); void ec.revealLocation(loc); }}
|
||||
// // title="reveal file location"></a>
|
||||
// // <a className="link pointer mh2 dim codicon codicon-quote"
|
||||
// // data-id="copy-to-comment"
|
||||
// // onClick={e => {e.preventDefault(); void ec.copyToComment(text)}}
|
||||
// // title="copy message to comment"></a>
|
||||
// // <a className="link pointer mh2 dim codicon codicon-clippy"
|
||||
// // onClick={e => {e.preventDefault(); void ec.api.copyToClipboard(text)}}
|
||||
// // title="copy message to clipboard"></a>
|
||||
// // </span>
|
||||
// // </summary>
|
||||
// <div className={severityClass + ' ml1 message'}>
|
||||
// {!(typewriterMode && !lockEditorMode) && <p className="mv2">{title}</p>}
|
||||
// <pre className="font-code pre-wrap">
|
||||
// <InteractiveMessage fmt={message} />
|
||||
// </pre>
|
||||
// </div>
|
||||
// // </details>
|
||||
// )
|
||||
// }, 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 (
|
||||
// <div>
|
||||
// {mkMessageViewProps(uri, messages).map(m => <MessageView {...m} />)}
|
||||
// </div>
|
||||
// );
|
||||
// })
|
||||
|
||||
// function lazy<T>(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<React.Dispatch<React.SetStateAction<boolean>>>();
|
||||
// useEvent(ec.events.requestedAction, act => {
|
||||
// if (act.kind === 'toggleAllMessages' && setOpenRef.current !== undefined) {
|
||||
// setOpenRef.current(t => !t);
|
||||
// }
|
||||
// });
|
||||
|
||||
// return (
|
||||
// <RpcContext.Provider value={rs}>
|
||||
// {/* <Details setOpenRef={setOpenRef as any} initiallyOpen={!config.autoOpenShowsGoal}>
|
||||
// <summary className="mv2 pointer">
|
||||
// All Messages ({diags.length})
|
||||
// <span className="fr">
|
||||
// <a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue' : 'codicon-debug-pause')}
|
||||
// onClick={e => { e.preventDefault(); setPaused(p => !p); }}
|
||||
// title={isPaused ? 'continue updating' : 'pause updating'}>
|
||||
// </a>
|
||||
// </span>
|
||||
// </summary> */}
|
||||
// <AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} curPos={curPos} />
|
||||
// {/* </Details> */}
|
||||
// </RpcContext.Provider>
|
||||
// )
|
||||
// }
|
||||
|
||||
// /** 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<InteractiveDiagnostic[]>}) {
|
||||
// let { t } = useTranslation()
|
||||
// const [msgs, setMsgs] = React.useState<InteractiveDiagnostic[] | undefined>(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 <div>{t("Loading messages…")}</div>
|
||||
// else return <MessagesList uri={uri} messages={msgs}/>
|
||||
// }
|
||||
|
||||
// /**
|
||||
// * 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<DocumentUri, Diagnostic[]>(),
|
||||
// async (params: PublishDiagnosticsParams) => diags =>
|
||||
// new Map(diags).set(params.uri, params.diagnostics),
|
||||
// []
|
||||
// )
|
||||
|
||||
// return <LspDiagnosticsContext.Provider value={allDiags}>{children}</LspDiagnosticsContext.Provider>
|
||||
// }
|
||||
|
||||
// /** Embeds a non-interactive diagnostic into the type `InteractiveDiagnostic`. */
|
||||
// export function lspDiagToInteractive(diag: Diagnostic): InteractiveDiagnostic {
|
||||
// return { ...(diag as LeanDiagnostic), message: { text: diag.message } };
|
||||
// }
|
||||
|
||||
@ -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<monaco.editor.IStandaloneCodeEditor>(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<HTMLFormElement> = (ev) => {
|
||||
ev.preventDefault()
|
||||
runCommand()
|
||||
}
|
||||
|
||||
// do not display if the proof is completed (with potential warnings still present)
|
||||
return <div className={`typewriter${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
|
||||
<form onSubmit={handleSubmit}>
|
||||
<div className="typewriter-input-wrapper">
|
||||
<div ref={inputRef} className="typewriter-input" />
|
||||
</div>
|
||||
<button type="submit" disabled={processing} className="btn btn-inverted">
|
||||
<FontAwesomeIcon icon={faWandMagicSparkles} /> {t("Execute")}
|
||||
</button>
|
||||
</form>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** 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<monaco.editor.IStandaloneCodeEditor>(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<HTMLFormElement> = (ev) => {
|
||||
// ev.preventDefault()
|
||||
// runCommand()
|
||||
// }
|
||||
|
||||
// // do not display if the proof is completed (with potential warnings still present)
|
||||
// return <div className={`typewriter${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
|
||||
// <form onSubmit={handleSubmit}>
|
||||
// <div className="typewriter-input-wrapper">
|
||||
// <div ref={inputRef} className="typewriter-input" />
|
||||
// </div>
|
||||
// <button type="submit" disabled={processing} className="btn btn-inverted">
|
||||
// <FontAwesomeIcon icon={faWandMagicSparkles} /> {t("Execute")}
|
||||
// </button>
|
||||
// </form>
|
||||
// </div>
|
||||
// }
|
||||
|
||||
// /** 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)
|
||||
// }
|
||||
// }
|
||||
|
||||
@ -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;
|
||||
}
|
||||
Loading…
Reference in New Issue