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

cleanup and scrolling

Browse Source
This commit is contained in:
Jon Eugster
2023-07-14 17:07:12 +02:00
parent 805b0b94c1
commit d0316b734a
6 changed files with 4549 additions and 356 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/infoview/command_line.tsx
+9 -4
View File
@@ -64,7 +64,7 @@ config.autoClosingPairs = config.autoClosingPairs.map(
monaco.languages.setLanguageConfiguration('lean4cmd', config);
/** The input field */
export function CommandLine() {
export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObject<HTMLDivElement>}) {
/** Reference to the hidden multi-line editor */
const editor = React.useContext(MonacoEditorContext)
@@ -74,7 +74,7 @@ export function CommandLine() {
const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
const [processing, setProcessing] = useState(false)
const { commandLineMode, commandLineInput, setCommandLineInput } = React.useContext(InputModeContext)
const {commandLineInput, setCommandLineInput} = React.useContext(InputModeContext)
const inputRef = useRef()
@@ -87,7 +87,7 @@ export function CommandLine() {
/** Load all goals an messages of the current proof (line-by-line) and save
* the retrieved information into context (`ProofContext`)
*/
const loadAllGoals = React.useCallback(() => {
const loadAllGoals = React.useCallback((proofPanelRef) => {
let goalCalls = []
let msgCalls = []
@@ -174,6 +174,8 @@ export function CommandLine() {
})
// Save the proof to the context
setProof(tmpProof)
console.debug('updated proof')
proofPanelRef.current?.lastElementChild?.scrollIntoView()
})
})
}, [commandLineInput, editor])
@@ -207,12 +209,15 @@ export function CommandLine() {
useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
if (params.uri == editor.getModel().uri.toString()) {
setProcessing(false)
loadAllGoals(proofPanelRef)
if (!hasErrors(params.diagnostics)) {
setCommandLineInput("")
editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
}
}
loadAllGoals() // TODO: instead of loading all goals every time, we could only load the last one
// 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()
}, []);
useEffect(() => {
client/src/components/infoview/infoview.css
+6
View File
@@ -135,6 +135,12 @@
.commandline-interface .content {
display: flex;
flex-direction: column;
scroll-behavior: smooth;
}
/* TODO this is in the wrong file */
.chat {
scroll-behavior: smooth;
}
.commandline-interface .content .tmp-pusher {
client/src/components/infoview/main.tsx
+80 -86
View File
@@ -31,36 +31,35 @@ import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from '
import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line';
import { InteractiveDiagnostic } from '@leanprover/infoview/*';
import { Button } from '../button';
import { CircularProgress } from '@mui/material';
/** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
* always present, or the monaco editor cannot start.
*/
export function DualEditor({level, codeviewRef, levelId, worldId, commandLineMode}) {
export function DualEditor({level, codeviewRef, levelId, worldId}) {
const ec = React.useContext(EditorContext)
// const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext)
// return <div className={hidden ? 'hidden' : ''}>
// <ExerciseStatement data={data} />
// <div className={`statement ${commandLineMode ? 'hidden' : ''}`}><code>{data?.descrFormat}</code></div>
// <div ref={codeviewRef} className={'codeview'}></div>
// {ec && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
// </div>
// }
const {commandLineMode} = React.useContext(InputModeContext)
return <>
<div className={commandLineMode ? ' hidden' : ''}>
<div className={commandLineMode ? 'hidden' : ''}>
<ExerciseStatement data={level?.data} />
<div ref={codeviewRef} className={'codeview'}></div>
</div>
{ec && <DualEditorMain worldId={worldId} levelId={levelId} level={level} commandLineMode={commandLineMode}/>}
{ec ?
<DualEditorMain worldId={worldId} levelId={levelId} level={level} /> :
// TODO: Style this if relevant.
<>
<p>Editor is starting up...</p>
<CircularProgress />
</>
}
</>
}
/* The part of the two editors that can needs the editor connection first */
function DualEditorMain({worldId, levelId, level, commandLineMode}) {
/** The part of the two editors that needs the editor connection first */
function DualEditorMain({worldId, levelId, level}) {
const ec = React.useContext(EditorContext)
const gameId = React.useContext(GameIdContext)
const {commandLineMode} = React.useContext(InputModeContext)
/* Set up updates to the global infoview state on editor events. */
const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
@@ -69,8 +68,8 @@ function DualEditorMain({worldId, levelId, level, commandLineMode}) {
'$/lean/fileProgress',
new Map<DocumentUri, LeanFileProgressProcessingInfo[]>(),
async (params: LeanFileProgressParams) => (allProgress) => {
const newProgress = new Map(allProgress);
return newProgress.set(params.textDocument.uri, params.processing);
const newProgress = new Map(allProgress);
return newProgress.set(params.textDocument.uri, params.processing);
}, [])
const serverVersion = useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? ''))
@@ -80,11 +79,6 @@ function DualEditorMain({worldId, levelId, level, commandLineMode}) {
<WithRpcSessions>
<WithLspDiagnosticsContext>
<ProgressContext.Provider value={allProgress}>
{/* We need the editor to always there and hidden because
the command line edits its content */}
{ // TODO: Is there any possibility that the editor connection takes a while
// and we should show a circular progress here?
}
{commandLineMode ?
<CommandLineInterface world={worldId} level={levelId} data={level?.data}/>
:
@@ -98,11 +92,12 @@ function DualEditorMain({worldId, levelId, level, commandLineMode}) {
</>
}
// 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
/** 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
*/
function ExerciseStatement({data}) {
if (!data?.descrText) { return <></> }
return <div className="exercise-statement"><Markdown>
@@ -276,24 +271,29 @@ export function CommandLineInterface(props: {world: string, level: number, data:
const ec = React.useContext(EditorContext)
const editor = React.useContext(MonacoEditorContext)
const gameId = React.useContext(GameIdContext)
const {proof} = React.useContext(ProofContext)
const proofPanelRef = React.useRef<HTMLDivElement>(null)
const dispatch = useAppDispatch()
// Mark level as completed when server gives notification
useServerNotificationEffect(
'$/game/completed',
(params: any) => {
'$/game/completed',
(params: any) => {
if (ec.events.changedCursorLocation.current &&
ec.events.changedCursorLocation.current.uri === params.uri) {
dispatch(levelCompleted({game: gameId, world: props.world, level: props.level}))
}
},
[]
);
if (ec.events.changedCursorLocation.current &&
ec.events.changedCursorLocation.current.uri === params.uri) {
dispatch(levelCompleted({game: gameId, world: props.world, level: props.level}))
}
}, []
)
// React.useEffect(() => {
// console.debug('updated proof')
// // proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
// }, [proof])
/** Delete all proof lines starting from a given line.
* Note that the first line (i.e. deleting everything) is `1`!
@@ -343,53 +343,47 @@ export function CommandLineInterface(props: {world: string, level: number, data:
// NB: the cursor may temporarily become `undefined` when a file is closed. In this case
// it's important not to reconstruct the `WithBlah` wrappers below since they contain state
// that we want to persist.
let ret
if (!serverVersion) {
ret = <p>Waiting for Lean server to start...</p>
} else if (serverStoppedResult){
ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
} else {
//className="infoview vscode-light"
ret = <div className="commandline-interface">
{/* {completed && <div className="level-completed">Level completed! 🎉</div>} */}
<div className="content">
<ExerciseStatement data={props.data} />
{/* <Infos /> */}
<div className="tmp-pusher"></div>
{proof.map((step, i) => {
if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) {
// if the last command contains an error, we should not display it
// as it will be overwritten by the next entered command
return <div>
<Errors errors={step.errors} commandLineMode={true}/>
</div>
}
else {
return <>
<div className="step">
<Command command={step.command} deleteProof={deleteProof(i)}/>
<Errors errors={step.errors} commandLineMode={true}/>
<GoalsTab proofStep={step}/>
</div>
{/* Show a message that there are no goals left */}
{!step.goals.length && (
<div className="message information">
{completed ?
<p>Level completed! 🎉</p> :
<p>
<b>no goals left</b><br />
<i>This probably means you solved the level with warnings</i>
</p>
}
</div>
)}
</>
}
})}
</div>
<CommandLine />
</div>
}
return ret
if (!serverVersion) {return <p>Waiting for Lean server to start...</p>}
if (serverStoppedResult) {return <div>
<p>{serverStoppedResult.message}</p>
<p className="error">{serverStoppedResult.reason}</p>
</div>}
return <div className="commandline-interface">
<div className="content" ref={proofPanelRef}>
<ExerciseStatement data={props.data} />
<div className="tmp-pusher"></div>
{proof.length ? proof.map((step, i) => {
if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) {
// if the last command contains an error, we only display the errors but not the
// entered command as it is still present in the command line.
return <div>
<Errors errors={step.errors} commandLineMode={true}/>
</div>
} else {
return <>
<div className="step">
<Command command={step.command} deleteProof={deleteProof(i)}/>
<Errors errors={step.errors} commandLineMode={true}/>
<GoalsTab proofStep={step}/>
</div>
{/* Show a message that there are no goals left */}
{!step.goals.length && (
<div className="message information">
{completed ?
<p>Level completed! 🎉</p> :
<p>
<b>no goals left</b><br />
<i>This probably means you solved the level with warnings</i>
</p>
}
</div>
)}
</>
}
}) : <CircularProgress />}
</div>
<CommandLine proofPanelRef={proofPanelRef}/>
</div>
}
client/src/components/level.tsx
+14 -7
View File
@@ -58,7 +58,7 @@ function Level() {
function PlayableLevel({worldId, levelId}) {
const codeviewRef = useRef<HTMLDivElement>(null)
const chatPanelRef = useRef<HTMLDivElement>(null)
const chatRef = useRef<HTMLDivElement>(null)
const gameId = React.useContext(GameIdContext)
@@ -77,13 +77,20 @@ function PlayableLevel({worldId, levelId}) {
const theme = useTheme();
useEffect(() => {
// Scroll to top when loading a new level
// TODO: Thats the wrong behaviour probably
chatPanelRef.current!.scrollTo(0,0)
// // Scroll to top when loading a new level
// // TODO: Thats the wrong behaviour probably
// chatRef.current!.scrollTo(0,0)
// Reset command line input when loading a new level
setCommandLineInput("")
}, [levelId])
useEffect(() => {
// TODO: For some reason this is always called twice
console.debug('scroll chat')
chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0)
}, [proof])
React.useEffect(() => {
if (!commandLineMode) {
// Delete last input attempt from command line
@@ -187,8 +194,8 @@ function PlayableLevel({worldId, levelId}) {
<ProofContext.Provider value={{proof, setProof}}>
<LevelAppBar isLoading={level.isLoading} levelTitle={levelTitle} worldId={worldId} levelId={levelId} />
<Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
<div ref={chatPanelRef} className="chat-panel">
<div className="chat">
<div className="chat-panel">
<div ref={chatRef} className="chat">
{level?.data?.introduction &&
<div className="message information">
<Markdown>{level?.data?.introduction}</Markdown>
@@ -225,7 +232,7 @@ function PlayableLevel({worldId, levelId}) {
<EditorContext.Provider value={editorConnection}>
<MonacoEditorContext.Provider value={editor}>
<div className="exercise">
<DualEditor level={level} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} commandLineMode={commandLineMode} />
<DualEditor level={level} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} />
</div>
</MonacoEditorContext.Provider>
</EditorContext.Provider>