update npm deps

bump npm dependencies
Update troubleshoot.md
2024-02-23 18:58:15 +01:00 · 2024-02-23 18:58:06 +01:00 · 2024-02-16 10:57:02 +01:00
19 changed files with 551 additions and 1095 deletions
@@ -1,9 +1,7 @@
-import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api";
+import { GameHint } from "./infoview/rpc_api";
 import * as React from 'react';
 import Markdown from './markdown';
-import { DeletedChatContext, ProofContext } from "./infoview/context";
+import { ProofStep } from "./infoview/context";
 import { lastStepHasErrors } from "./infoview/goals";
 import { Button } from "./button";
 export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
  return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
@@ -18,7 +16,7 @@ export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} :
 }
 export function Hints({hints, showHidden, step, selected, toggleSelection, lastLevel} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
-  if (!hints) {return <></>}
+
  const openHints = hints.filter(hint => !hint.hidden)
  const hiddenHints = hints.filter(hint => hint.hidden)
@@ -48,52 +46,22 @@ export function DeletedHints({hints} : {hints: GameHint[]}) {
 }
 /** Filter hints to not show consequtive identical hints twice.
- * Hidden hints are not filtered.
+ *
 * This function takes a `ProofStep[]` and extracts the hints in form of an
 * element of type `GameHint[][]` where it removes hints that are identical to hints
 * appearing in the previous step. Hidden hints are not filtered.
 *
 * This effectively means we prevent consequtive identical hints from being shown.
 */
-export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
+export function filterHints(proof: ProofStep[]): GameHint[][] {
-  if (!hints) {
+  return proof.map((step, i) => {
-    return []}
+    if (i == 0){
-  else if (!prevHints) {
+      return step.hints
    return hints }
  else {
    return hints.filter((hint) => hint.hidden ||
    (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
    )
  }
 }
 function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
  return step?.goals[0]?.hints.some((hint) => hint.hidden)
 }
 export function MoreHelpButton({selected=null} : {selected?: number}) {
  const {proof, setProof} = React.useContext(ProofContext)
  const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
  let k = (selected === null) ? (proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected
  const activateHiddenHints = (ev) => {
    // If the last step (`k`) has errors, we want the hidden hints from the
    // second-to-last step to be affected
    if (!(proof.steps.length)) {return}
    // state must not be mutated, therefore we need to clone the set
    let tmp = new Set(showHelp)
    if (tmp.has(k)) {
      tmp.delete(k)
    } else {
-      tmp.add(k)
+      // TODO: Writing all fields explicitely is somewhat fragile to changes, is there a
      // good way to shallow-compare objects?
      return step.hints.filter((hint) => hint.hidden ||
        (proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined))
    }
-    setShowHelp(tmp)
+  })
    console.debug(`help: ${Array.from(tmp.values())}`)
  }
  if (hasHiddenHints(proof.steps[k]) && !showHelp.has(k)) {
    return <Button to="" onClick={activateHiddenHints}>
      Show more help!
    </Button>
  }
 }
@@ -3,8 +3,8 @@
 */
 import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { InteractiveDiagnostic } from '@leanprover/infoview-api';
+import { InteractiveDiagnostic, InteractiveTermGoal } from '@leanprover/infoview-api';
-import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
+import { GameHint, InteractiveGoal, InteractiveGoals } from './rpc_api';
 import { PreferencesState } from '../../state/preferences';
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
@@ -12,39 +12,37 @@ export const MonacoEditorContext = React.createContext<monaco.editor.IStandalone
 export type InfoStatus = 'updating' | 'error' | 'ready';
-// /** One step of the proof */
+/** One step of the proof */
-// export type ProofStep = {
+export type ProofStep = {
-//   /** The command in this step */
+  /** The command in this step */
-//   command : string
+  command : string
-//   /** List of goals *after* this command */
+  /** List of goals *after* this command */
-//   goals: InteractiveGoal[]     // TODO: Add correct type
+  goals: InteractiveGoal[]     // TODO: Add correct type
-//   /** Story relevant messages */
+  /** Story relevant messages */
-//   hints: GameHint[]        // TODO: Add correct type
+  hints: GameHint[]        // TODO: Add correct type
-//   /** Errors and warnings */
+  /** Errors and warnings */
-//   errors: InteractiveDiagnostic[]       // TODO: Add correct type
+  errors: InteractiveDiagnostic[]       // TODO: Add correct type
-// }
+}
 /** The context storing the proof step-by-step for the command line mode */
 export const ProofContext = React.createContext<{
  /** The proof consists of multiple steps that are processed one after the other.
   * In particular multi-line terms like `match`-statements will not be supported.
   *
-   * Note that the first step will always have "" as command
+   * Note that the first step will always have `null` as command
   */
-  proof: ProofState,
+  proof: ProofStep[],
-  setProof: React.Dispatch<React.SetStateAction<ProofState>>
+  setProof: React.Dispatch<React.SetStateAction<Array<ProofStep>>>
 }>({
-  proof: {steps: [], diagnostics: [], completed: false},
+  proof: [],
-  setProof: () => {}
+  setProof: () => {} // TODO: implement me
 })
 // TODO: Do we still need that?
 export interface ProofStateProps {
  // pos: DocumentPosition;
  status: InfoStatus;
  messages: InteractiveDiagnostic[];
-  goals?: InteractiveGoalsWithHints;
+  goals?: InteractiveGoals;
  termGoal?: InteractiveTermGoal;
  error?: string;
  // userWidgets: UserWidgetInstance[];
@@ -52,18 +50,18 @@ export interface ProofStateProps {
  // triggerUpdate: () => Promise<void>;
 }
-// export const ProofStateContext = React.createContext<{
+export const ProofStateContext = React.createContext<{
-//   proofState : ProofStateProps,
+  proofState : ProofStateProps,
-//   setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
+  setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
-// }>({
+}>({
-//   proofState : {
+  proofState : {
-//     status: 'updating',
+    status: 'updating',
-//     messages: [],
+    messages: [],
-//     goals: undefined,
+    goals: undefined,
-//     termGoal: undefined,
+    termGoal: undefined,
-//     error: undefined},
+    error: undefined},
-//   setProofState: () => {},
+  setProofState: () => {},
-// })
+})
 export interface IPreferencesContext extends PreferencesState{
  mobile: boolean, // The variables that actually control the page 'layout' can only be changed through layout.
@@ -10,10 +10,7 @@ import { Locations, LocationsContext, SelectableLocation } from '../../../../nod
 import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
 import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
 import { InputModeContext } from './context';
-import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api';
+import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api';
 import { RpcSessionAtPos } from '@leanprover/infoview/*';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { DiagnosticSeverity } from 'vscode-languageserver-protocol';
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -42,11 +39,7 @@ function goalToString(g: InteractiveGoal): string {
 }
 export function goalsToString(goals: InteractiveGoals): string {
-    return goals.goals.map(g => goalToString(g)).join('\n\n')
+    return goals.goals.map(goalToString).join('\n\n')
 }
 export function goalsWithHintsToString(goals: InteractiveGoalsWithHints): string {
    return goals.goals.map(g => goalToString(g.goal)).join('\n\n')
 }
 interface GoalFilterState {
@@ -262,7 +255,7 @@ export const ProofDisplay = React.memo((props : ProofDisplayProps) => {
 })
 interface GoalsProps {
-    goals: InteractiveGoalsWithHints
+    goals: InteractiveGoals
    filter: GoalFilterState
 }
@@ -271,7 +264,7 @@ export function Goals({ goals, filter }: GoalsProps) {
        return <>No goals</>
    } else {
        return <>
-          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}
+          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g} filter={filter} />)}
        </>
    }
 }
@@ -283,7 +276,7 @@ interface FilteredGoalsProps {
     * 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
+    goals?: InteractiveGoals
 }
 /**
@@ -298,7 +291,7 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
            data-id="copy-goal-to-comment"
            onClick={e => {
                e.preventDefault();
-                if (goals) void ec.copyToComment(goalsWithHintsToString(goals))
+                if (goals) void ec.copyToComment(goalsToString(goals))
            }}
            title="copy state to comment" />
@@ -343,112 +336,3 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
        </details>
    </div>
 })
 export function loadGoals(
    rpcSess: RpcSessionAtPos,
    uri: string,
    setProof: React.Dispatch<React.SetStateAction<ProofState>>) {
  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) => {
      console.info(`received a proof state!`)
      console.log(proof)
      setProof(proof)
      // let tmpProof : ProofStep[] = []
      // let goalCount = 0
      // steps.map((goals, i) => {
      //   // The first step has an empty command and therefore also no error messages
      //   // Usually there is a newline at the end of the editors content, so we need to
      //   // display diagnostics from potentally two lines in the last step.
      //   let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
      //   // Filter out the 'unsolved goals' message
      //   messages = messages.filter((msg) => {
      //     return !("append" in msg.message &&
      //       "text" in msg.message.append[0] &&
      //       msg.message.append[0].text === "unsolved goals")
      //   })
      //   if (typeof goals == 'undefined') {
      //     tmpProof.push({
      //       command: i ? model.getLineContent(i) : '',
      //       goals: [],
      //       hints: [],
      //       errors: messages
      //     } as ProofStep)
      //     console.debug('goals is undefined')
      //     return
      //   }
      //   // If the number of goals reduce, show a message
      //   if (goals.length && goalCount > goals.length) {
      //     messages.unshift({
      //       range: {
      //         start: {
      //           line: i-1,
      //           character: 0,
      //         },
      //         end: {
      //           line: i-1,
      //           character: 0,
      //         }},
      //       severity: DiagnosticSeverity.Information,
      //       message: {
      //       text: 'intermediate goal solved 🎉'
      //       }
      //     })
      //   }
      //   goalCount = goals.length
      //   // with no goals there will be no hints.
      //   let hints : GameHint[] = goals.length ? goals[0].hints : []
      //   console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
      //   console.debug(`Goals: (${i}): `, goalsToString(goals)) //
      //   console.debug(`Hints: (${i}): `, hints)
      //   console.debug(`Errors: (${i}): `, messages)
      //   tmpProof.push({
      //     // the command of the line above. Note that `getLineContent` starts counting
      //     // at `1` instead of `zero`. The first ProofStep will have an empty command.
      //     command: i ? model.getLineContent(i) : '',
      //     // TODO: store correct data
      //     goals: goals.map(g => g.goal),
      //     // only need the hints of the active goals in chat
      //     hints: hints,
      //     // errors and messages from the server
      //     errors: messages
      //   } as ProofStep)
      // })
      // // Save the proof to the context
      // setProof(tmpProof)
    }
  )
 }
 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)
 }
@@ -4,7 +4,7 @@ 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'
+  RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } 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'
@@ -14,7 +14,7 @@ import { GoalsLocation, Locations, LocationsContext } from '../../../../node_mod
 import { AllMessages, lspDiagToInteractive } from './messages'
 import { goalsToString, Goal, MainAssumptions, OtherGoals, ProofDisplay } from './goals'
-import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api'
+import { InteractiveGoals } from './rpc_api'
 import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from './context'
 // TODO: All about pinning could probably be removed
@@ -83,11 +83,11 @@ interface InfoDisplayContentProps extends PausableProps {
  error?: string
  userWidgets: UserWidgetInstance[]
  triggerUpdate: () => Promise<void>
-  proofString? : string
+  proof? : string
 }
 const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
-    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props
+    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proof} = props
    const hasWidget = userWidgets.length > 0
    const hasError = !!error
@@ -114,8 +114,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
    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 <>
   return <>
        {hasError &&
            <div className='error' key='errors'>
                Error updating:{' '}{error}.
@@ -138,7 +137,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
        {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 : []}
+            <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals.map (goal => goal) : []}
              termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
          </details>
        )}
@@ -167,7 +166,6 @@ interface InfoDisplayProps {
  pos: DocumentPosition,
  status: InfoStatus,
  messages: InteractiveDiagnostic[],
  proof?: ProofState,
  goals?: InteractiveGoals,
  termGoal?: InteractiveTermGoal,
  error?: string,
@@ -177,7 +175,7 @@ interface InfoDisplayProps {
 }
 /** Displays goal state and messages. Can be paused. */
-function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
+function InfoDisplay(props0: ProofStateProps & 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)
@@ -216,7 +214,7 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
    {/* <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} />
+            <InfoDisplayContent {...props} proof={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
        </div>
    {/* </details> */}
    </RpcContext.Provider>
@@ -254,7 +252,7 @@ function useIsProcessingAt(p: DocumentPosition): boolean {
 function InfoAux(props: InfoProps) {
-    const { setProof } = React.useContext(ProofContext)
+    const proofContext = React.useContext(ProofContext)
    const config = React.useContext(ConfigContext)
@@ -292,8 +290,6 @@ function InfoAux(props: InfoProps) {
    // 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))
        const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos))
        const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos))
        const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound)
@@ -312,7 +308,6 @@ function InfoAux(props: InfoProps) {
                pos,
                status: 'updating',
                messages: lspDiagsHere.map(lspDiagToInteractive),
                proof: undefined,
                goals: undefined,
                termGoal: undefined,
                error: undefined,
@@ -323,12 +318,11 @@ function InfoAux(props: InfoProps) {
        // 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(
+        Promise.all([goalsReq, termGoalReq, widgetsReq, messagesReq]).then(
-            ([proof, goals, termGoal, userWidgets, messages]) => resolve({
+            ([goals, termGoal, userWidgets, messages]) => resolve({
                pos,
                status: 'ready',
                messages,
                proof : proof as any,
                goals: goals as any,
                termGoal,
                error: undefined,
@@ -359,7 +353,6 @@ function InfoAux(props: InfoProps) {
                    pos,
                    status: 'error',
                    messages: lspDiagsHere.map(lspDiagToInteractive),
                    proof: undefined,
                    goals: undefined,
                    termGoal: undefined,
                    error: `Error fetching goals: ${errorString}`,
@@ -396,7 +389,6 @@ function InfoAux(props: InfoProps) {
        pos,
        status: 'updating',
        messages: [],
        proof: undefined,
        goals: undefined,
        termGoal: undefined,
        error: undefined,
@@ -420,11 +412,6 @@ function InfoAux(props: InfoProps) {
          //   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)
@@ -26,16 +26,15 @@ import Markdown from '../markdown';
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
-import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals';
+import { Goal } from './goals';
-import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context';
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
-import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter';
+import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
-import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
+import { GameHint } from './rpc_api';
 import { store } from '../../state/store';
-import { Hints, MoreHelpButton, filterHints } from '../hints';
+import { Hints, filterHints } from '../hints';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
 * always present, or the monaco editor cannot start.
@@ -62,35 +61,36 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
  const gameId = React.useContext(GameIdContext)
  const { typewriterMode } = React.useContext(InputModeContext)
-  const {proof, setProof} = React.useContext(ProofContext)
+  // Mark level as completed when server gives notification
  const dispatch = useAppDispatch()
  useServerNotificationEffect(
    '$/game/completed',
    (params: any) => {
      if (ec.events.changedCursorLocation.current &&
          ec.events.changedCursorLocation.current.uri === params.uri) {
        dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
-  React.useEffect(() => {
+        // On completion, add the names of all new items to the local storage
-    if (proof.completed) {
+        let newTiles = [
-      dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
+          ...level?.tactics,
          ...level?.lemmas,
          ...level?.definitions
        ].filter((tile) => tile.new).map((tile) => tile.name)
-      // On completion, add the names of all new items to the local storage
+        // Add the proven statement to the local storage as well.
-      let newTiles = [
+        if (level?.statementName != null) {
-        ...level?.tactics,
+          newTiles.push(level?.statementName)
-        ...level?.lemmas,
+        }
        ...level?.definitions
      ].filter((tile) => tile.new).map((tile) => tile.name)
-      // Add the proven statement to the local storage as well.
+        let inv: string[] = selectInventory(gameId)(store.getState())
-      if (level?.statementName != null) {
+
-        newTiles.push(level?.statementName)
+        // add new items and remove duplicates
        let newInv = [...inv, ...newTiles].filter((item, i, array) => array.indexOf(item) == i)
        dispatch(changedInventory({ game: gameId, inventory: newInv }))
      }
-
+    }, [level]
-      let inv: string[] = selectInventory(gameId)(store.getState())
+  )
      // add new items and remove duplicates
      let newInv = [...inv, ...newTiles].filter((item, i, array) => array.indexOf(item) == i)
      dispatch(changedInventory({ game: gameId, inventory: newInv }))
    }
  }, [proof, level])
  /* Set up updates to the global infoview state on editor events. */
  const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
@@ -154,21 +154,8 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
  const gameId = React.useContext(GameIdContext)
  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
-  const { proof, setProof } = React.useContext(ProofContext)
+  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
  const {selectedStep, setSelectedStep} = React.useContext(SelectionContext)
  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
  function toggleSelection(line: number) {
    return (ev) => {
      console.debug('toggled selection')
      if (selectedStep == line) {
        setSelectedStep(undefined)
      } else {
        setSelectedStep(line)
      }
    }
  }
  console.debug(`template: ${props.data?.template}`)
  // React.useEffect (() => {
@@ -195,19 +182,6 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
  const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
  const curPos: DocumentPosition | undefined =
    useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined)
  // Effect when the cursor changes in the editor
  React.useEffect(() => {
    // TODO: this is a bit of a hack and will yield unexpected behaviour if lines
    // are indented.
    let newPos = curPos?.line + (curPos?.character == 0 ? 0 : 1)
    // scroll the chat along
    setSelectedStep(newPos)
  }, [curPos])
  useClientNotificationEffect(
    'textDocument/didClose',
    (params: DidCloseTextDocumentParams) => {
@@ -232,13 +206,8 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
    ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
  } else {
    ret = <div className="infoview vscode-light">
-      {proof.completed && <div className="level-completed">Level completed! 🎉</div>}
+      {completed && <div className="level-completed">Level completed! 🎉</div>}
      <Infos />
      <Hints hints={proof.steps[curPos?.line]?.goals[0]?.hints}
        showHidden={showHelp.has(curPos?.line)} step={curPos?.line}
        selected={selectedStep} toggleSelection={toggleSelection(curPos?.line)}
        lastLevel={curPos?.line == proof.steps.length - 1}/>
      <MoreHelpButton selected={curPos?.line}/>
    </div>
  }
@@ -254,24 +223,15 @@ const goalFilter = {
 }
 /** The display of a single entered lean command */
-function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) {
+function Command({ command, deleteProof }: { command: string, deleteProof: any }) {
  // The first step will always have an empty command
-  if (!proof?.steps[i]?.command) { return <></> }
+  if (!command) { return <></> }
-
+  return <div className="command">
-  if (isLastStepWithErrors(proof, i)) {
+    <div className="command-text">{command}</div>
-    // If the last step has errors, we display the command in a different style
+    <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
-    // indicating that it will be removed on the next try.
+      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
-    return <div className="failed-command">
+    </Button>
-      <i>Failed command</i>: {proof.steps[i].command}
+  </div>
    </div>
  } else {
    return <div className="command">
      <div className="command-text">{proof.steps[i].command}</div>
      <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
        <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
      </Button>
    </div>
  }
 }
 // const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
@@ -326,14 +286,10 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
 // }, fastIsEqual)
 /** The tabs of goals that lean ahs after the command of this step has been processed */
-function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
+function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: ProofStep, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
  const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
  if (proofStep.goals.length == 0) {
    return <></>
  }
  return <div className="goal-tabs" onClick={onClick}>
    <div className={`tab-bar ${last ? 'current' : ''}`}>
      {proofStep.goals.map((goal, i) => (
@@ -344,7 +300,7 @@ function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofSte
      ))}
    </div>
    <div className="goal-tab vscode-light">
-      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]?.goal} />
+      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
    </div>
  </div>
 }
@@ -394,11 +350,12 @@ export function TypewriterInterface({props}) {
  const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
  const {mobile} = React.useContext(PreferencesContext)
-  const { proof, setProof } = React.useContext(ProofContext)
+  const { proof } = React.useContext(ProofContext)
  const { setTypewriterInput } = React.useContext(InputModeContext)
  const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
  const proofPanelRef = React.useRef<HTMLDivElement>(null)
  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
  // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
  // const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
@@ -410,11 +367,9 @@ export function TypewriterInterface({props}) {
  function deleteProof(line: number) {
    return (ev) => {
      let deletedChat: Array<GameHint> = []
-      proof.steps.slice(line).map((step, i) => {
+      filterHints(proof).slice(line).map((hintsAtStep, i) => {
        let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
        // Only add these hidden hints to the deletion stack which were visible
-        deletedChat = [...deletedChat, ...filteredHints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+        deletedChat = [...deletedChat, ...hintsAtStep.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
      })
      setDeletedChat(deletedChat)
@@ -427,9 +382,7 @@ export function TypewriterInterface({props}) {
        forceMoveMarkers: false
      }])
      setSelectedStep(undefined)
-      setTypewriterInput(proof.steps[line].command)
+      setTypewriterInput(proof[line].command)
      // Reload proof on deleting
      loadGoals(rpcSess, uri, setProof)
      ev.stopPropagation()
    }
  }
@@ -449,7 +402,7 @@ export function TypewriterInterface({props}) {
   // Scroll to the end of the proof if it is updated.
   React.useEffect(() => {
-    if (proof.steps.length > 1) {
+    if (proof?.length > 1) {
      proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
    } else {
      proofPanelRef.current?.scrollTo(0,0)
@@ -470,8 +423,38 @@ export function TypewriterInterface({props}) {
    }
  }, [selectedStep])
-  // TODO: superfluous, can be replaced with `withErr` from above
+  // TODO: This about hidden hints is all copied from `level.tsx`. Can we move that into `hints.tsx`?
-  let lastStepErrors = proof.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof.steps.length)) : false
+
  // If the last step has errors, we want to treat it as if it is part of the second-to-last step
  let k = proof.length - 1
  let withErr = hasInteractiveErrors(proof[k]?.errors) ? 1 : 0
  const activateHiddenHints = (ev) => {
    // If the last step (`k`) has errors, we want the hidden hints from the
    // second-to-last step to be affected
    if (!(proof.length)) {return}
    // state must not be mutated, therefore we need to clone the set
    let tmp = new Set(showHelp)
    if (tmp.has(k - withErr)) {
      tmp.delete(k - withErr)
    } else {
      tmp.add(k - withErr)
    }
    setShowHelp(tmp)
    console.debug(`help: ${Array.from(tmp.values())}`)
  }
  function hasHiddenHints(i : number): boolean {
    let step = proof[i]
    // For example if the proof isn't loaded yet
    if(!step) {return false}
    return step.hints.some((hint) => hint.hidden)
  }
  let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false
  useServerNotificationEffect("$/game/loading", (params : any) => {
@@ -491,22 +474,20 @@ export function TypewriterInterface({props}) {
      </div>
      <div className='proof' ref={proofPanelRef}>
        <ExerciseStatement data={props.data} />
-        {proof.steps.length ?
+        {proof.length ?
          <>
-            {proof.steps.map((step, i) => {
+            {proof.map((step, i) => {
-              let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
+              if (i == proof.length - 1 && lastStepErrors) {
-
+                // if the last command contains an error, we only display the errors but not the
-              // if (i == proof.steps.length - 1 && hasInteractiveErrors(step.diags)) {
+                // entered command as it is still present in the command line.
-              //   // if the last command contains an error, we only display the errors but not the
+                // TODO: Should not use index as key.
-              //   // entered command as it is still present in the command line.
+                return <div key={`proof-step-${i}`}>
-              //   // TODO: Should not use index as key.
+                  <Errors errors={step.errors} typewriterMode={true} />
-              //   return <div key={`proof-step-${i}`} className={`step step-${i}`}>
+                </div>
-              //     <Errors errors={step.diags} typewriterMode={true} />
+              } else {
              //   </div>
              // } else {
                return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
-                  <Command proof={proof} i={i} deleteProof={deleteProof(i)} />
+                  <Command command={step.command} deleteProof={deleteProof(i)} />
-                  <Errors errors={step.diags} typewriterMode={true} />
+                  <Errors errors={step.errors} typewriterMode={true} />
                  {mobile && i == 0 && props.data?.introduction &&
                    <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
                      <Markdown>{props.data?.introduction}</Markdown>
@@ -514,21 +495,22 @@ export function TypewriterInterface({props}) {
                  }
                  {mobile &&
                    <Hints key={`hints-${i}`}
-                      hints={filteredHints} showHidden={showHelp.has(i)} step={i}
+                      hints={step.hints} showHidden={showHelp.has(i)} step={i}
                      selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
                  }
-                  {/* <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
+                  <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
-                  {!(isLastStepWithErrors(proof, i)) &&
+
-                    <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+                  {mobile && i == proof.length - 1 &&
-                  }
+                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-                  {mobile && i == proof.steps.length - 1 &&
+                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
-                    <MoreHelpButton />
+                      Show more help!
                    </Button>
                  }
                  {/* Show a message that there are no goals left */}
-                  {/* {!step.goals.length && (
+                  {!step.goals.length && (
                    <div className="message information">
-                      {proof.completed ?
+                      {completed ?
                        <p>Level completed! 🎉</p> :
                        <p>
                          <b>no goals left</b><br />
@@ -536,17 +518,11 @@ export function TypewriterInterface({props}) {
                        </p>
                      }
                    </div>
-                  )} */}
+                  )}
                </div>
              }
-            //}
+            })}
-            )}
+            {mobile && completed &&
            {proof.diagnostics.length > 0 &&
              <div key={`proof-step-remaining`} className="step step-remaining">
                <Errors errors={proof.diagnostics} typewriterMode={true} />
              </div>
            }
            {mobile && proof.completed &&
              <div className="button-row mobile">
                {props.level >= props.worldSize ?
                  <Button to={`/${gameId}`}>
@@ -563,7 +539,7 @@ export function TypewriterInterface({props}) {
        }
      </div>
    </div>
-    <Typewriter disabled={disableInput || !proof.steps.length}/>
+    <Typewriter hidden={!withErr && proof[proof.length - 1]?.goals.length == 0} disabled={disableInput || !proof.length}/>
    </RpcContext.Provider>
  </div>
 }
@@ -194,24 +194,16 @@ export function AllMessages() {
                </a>
            </span>
        </summary> */}
-        <AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} curPos={curPos} />
+        <AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} />
    {/* </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[]>}) {
+function AllMessagesBody({uri, messages}: {uri: DocumentUri, messages: () => Promise<InteractiveDiagnostic[]>}) {
    const [msgs, setMsgs] = React.useState<InteractiveDiagnostic[] | undefined>(undefined)
-    React.useEffect(() => { void messages().then(
+    React.useEffect(() => { void messages().then(setMsgs) }, [messages])
        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>Loading messages...</div>
    else return <MessagesList uri={uri} messages={msgs}/>
 }
@@ -3,80 +3,46 @@
 *
 * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts`
 */
-import type { Range } from 'vscode-languageserver-protocol';
+import { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
 import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
 import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*';
 import type { Diagnostic } from 'vscode-languageserver-protocol';
 export interface InteractiveHypothesisBundle {
  /** The pretty names of the variables in the bundle. Anonymous names are rendered
   * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
   * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */
  names: string[];
  fvarIds?: FVarId[];
  type: CodeWithInfos;
  val?: CodeWithInfos;
  isInstance?: boolean;
  isType?: boolean;
  isInserted?: boolean;
  isRemoved?: boolean;
  isAssumption?: boolean;
 }
 export interface InteractiveGoalCore {
  hyps: InteractiveHypothesisBundle[];
  type: CodeWithInfos;
  ctx?: ContextInfo;
 }
 export interface InteractiveGoal extends InteractiveGoalCore {
  userName?: string;
  goalPrefix?: string;
  mvarId?: MVarId;
  isInserted?: boolean;
  isRemoved?: boolean;
 }
 export interface InteractiveGoals extends InteractiveGoalCore {
  goals: InteractiveGoals[];
 }
 export interface InteractiveTermGoal extends InteractiveGoalCore {
  range?: Range;
  term?: TermInfo;
 }
 export interface GameHint {
  text: string;
  hidden: boolean;
 }
-export interface InteractiveGoalWithHints {
+export interface InteractiveHypothesisBundle {
-  goal: InteractiveGoal;
+  /** The pretty names of the variables in the bundle. Anonymous names are rendered
   * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
   * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */
  names: string[];
  /** Present since server version 1.1.2. */
  fvarIds?: FVarId[];
  type: CodeWithInfos;
  val?: CodeWithInfos;
  isInstance?: boolean;
  isType?: boolean;
  isAssumption?: boolean;
  isInserted?: boolean;
  isRemoved?: boolean;
 }
 export interface InteractiveGoalCore {
  hyps: InteractiveHypothesisBundle[];
  type: CodeWithInfos;
  /** Present since server version 1.1.2. */
  ctx?: ContextInfo;
 }
 export interface InteractiveGoal extends InteractiveGoalCore {
  userName?: string;
  goalPrefix?: string;
  /** Present since server version 1.1.2. */
  mvarId?: MVarId;
  isInserted?: boolean;
  isRemoved?: boolean;
  hints: GameHint[];
 }
-export interface InteractiveGoalsWithHints {
+export interface InteractiveGoals {
-  goals: InteractiveGoalWithHints[];
+  goals: InteractiveGoal[];
  command: string;
  diags: InteractiveDiagnostic[];
 }
 /**
 * The proof state as it is received from the server.
 * Per proof step of the tactic proof, there is one `InteractiveGoalWithHints[]`.
 */
 export interface ProofState {
  /** The proof steps. step 0 is the state at the beginning of the proof. step one
   * contains the goal after the first line has been evaluated.
   *
   * In particular `step[i]` is the proof step at the beginning of line `i` in vscode.
   */
  steps: InteractiveGoalsWithHints[];
  /** The remaining diagnostics that are not in the steps. Usually this should only
   * be the "unsolved goals" message, I believe.
   */
  diagnostics : InteractiveDiagnostic[];
  completed : Boolean;
  completedWithWarnings : Boolean;
 }
@@ -5,7 +5,7 @@ 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 { DiagnosticSeverity, PublishDiagnosticsParams } 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';
@@ -13,21 +13,13 @@ 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 { InteractiveDiagnostic, 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 { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext } from './context'
+import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context'
-import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
+import { goalsToString } from './goals'
-import { GameHint, ProofState } from './rpc_api'
+import { GameHint, InteractiveGoals } from './rpc_api'
 export interface GameDiagnosticsParams {
  uri: DocumentUri;
  diagnostics: Diagnostic[];
 }
 /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
@@ -72,7 +64,7 @@ config.autoClosingPairs = config.autoClosingPairs.map(
 monaco.languages.setLanguageConfiguration('lean4cmd', config);
 /** The input field */
-export function Typewriter({disabled}: {disabled?: boolean}) {
+export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boolean}) {
  /** Reference to the hidden multi-line editor */
  const editor = React.useContext(MonacoEditorContext)
@@ -97,98 +89,98 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
  /** 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(() => {
-  //   let goalCalls = []
+    let goalCalls = []
-  //   let msgCalls = []
+    let msgCalls = []
-  //   // For each line of code ask the server for the goals and the messages on this line
+    // For each line of code ask the server for the goals and the messages on this line
-  //   for (let i = 0; i < model.getLineCount(); i++) {
+    for (let i = 0; i < model.getLineCount(); i++) {
-  //     goalCalls.push(
+      goalCalls.push(
-  //       rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
+        rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
-  //     )
+      )
-  //     msgCalls.push(
+      msgCalls.push(
-  //       getInteractiveDiagnostics(rpcSess, {start: i, end: i+1}).catch((error) => {console.debug("promise broken")})
+        getInteractiveDiagnostics(rpcSess, {start: i, end: i+1}).catch((error) => {console.debug("promise broken")})
-  //     )
+      )
-  //   }
+    }
-  //   // Wait for all these requests to be processed before saving the results
+    // Wait for all these requests to be processed before saving the results
-  //   Promise.all(goalCalls).then((steps : InteractiveGoalsWithHints[]) => {
+    Promise.all(goalCalls).then((steps : InteractiveGoals[]) => {
-  //     Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
+      Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
-  //       let tmpProof : ProofStep[] = []
+        let tmpProof : ProofStep[] = []
-  //       let goalCount = 0
+        let goalCount = 0
-  //       steps.map((goals, i) => {
+        steps.map((goals, i) => {
-  //         // The first step has an empty command and therefore also no error messages
+          // The first step has an empty command and therefore also no error messages
-  //         // Usually there is a newline at the end of the editors content, so we need to
+          // Usually there is a newline at the end of the editors content, so we need to
-  //         // display diagnostics from potentally two lines in the last step.
+          // display diagnostics from potentally two lines in the last step.
-  //         let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
+          let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
-  //         // Filter out the 'unsolved goals' message
+          // Filter out the 'unsolved goals' message
-  //         messages = messages.filter((msg) => {
+          messages = messages.filter((msg) => {
-  //           return !("append" in msg.message &&
+            return !("append" in msg.message &&
-  //             "text" in msg.message.append[0] &&
+              "text" in msg.message.append[0] &&
-  //             msg.message.append[0].text === "unsolved goals")
+              msg.message.append[0].text === "unsolved goals")
-  //         })
+          })
-  //         if (typeof goals == 'undefined') {
+          if (typeof goals == 'undefined') {
-  //           tmpProof.push({
+            tmpProof.push({
-  //             command: i ? model.getLineContent(i) : '',
+              command: i ? model.getLineContent(i) : '',
-  //             goals: [],
+              goals: [],
-  //             hints: [],
+              hints: [],
-  //             errors: messages
+              errors: messages
-  //           } as ProofStep)
+            } as ProofStep)
-  //           console.debug('goals is undefined')
+            console.debug('goals is undefined')
-  //           return
+            return
-  //         }
+          }
-  //         // If the number of goals reduce, show a message
+          // If the number of goals reduce, show a message
-  //         if (goals.length && goalCount > goals.length) {
+          if (goals.goals.length && goalCount > goals.goals.length) {
-  //           messages.unshift({
+            messages.unshift({
-  //             range: {
+              range: {
-  //               start: {
+                start: {
-  //                 line: i-1,
+                  line: i-1,
-  //                 character: 0,
+                  character: 0,
-  //               },
+                },
-  //               end: {
+                end: {
-  //                 line: i-1,
+                  line: i-1,
-  //                 character: 0,
+                  character: 0,
-  //               }},
+                }},
-  //             severity: DiagnosticSeverity.Information,
+              severity: DiagnosticSeverity.Information,
-  //             message: {
+              message: {
-  //             text: 'intermediate goal solved 🎉'
+              text: 'intermediate goal solved 🎉'
-  //             }
+              }
-  //           })
+            })
-  //         }
+          }
-  //         goalCount = goals.length
+          goalCount = goals.goals.length
-  //         // with no goals there will be no hints.
+          // with no goals there will be no hints.
-  //         let hints : GameHint[] = goals.length ? goals[0].hints : []
+          let hints : GameHint[] = goals.goals.length ? goals.goals[0].hints : []
-  //         console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
+          console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
-  //         console.debug(`Goals: (${i}): `, goalsToString(goals)) //
+          console.debug(`Goals: (${i}): `, goalsToString(goals)) //
-  //         console.debug(`Hints: (${i}): `, hints)
+          console.debug(`Hints: (${i}): `, hints)
-  //         console.debug(`Errors: (${i}): `, messages)
+          console.debug(`Errors: (${i}): `, messages)
-  //         tmpProof.push({
+          tmpProof.push({
-  //           // the command of the line above. Note that `getLineContent` starts counting
+            // the command of the line above. Note that `getLineContent` starts counting
-  //           // at `1` instead of `zero`. The first ProofStep will have an empty command.
+            // at `1` instead of `zero`. The first ProofStep will have an empty command.
-  //           command: i ? model.getLineContent(i) : '',
+            command: i ? model.getLineContent(i) : '',
-  //           // TODO: store correct data
+            // TODO: store correct data
-  //           goals: goals.map(g => g.goal),
+            goals: goals.goals,
-  //           // only need the hints of the active goals in chat
+            // only need the hints of the active goals in chat
-  //           hints: hints,
+            hints: hints,
-  //           // errors and messages from the server
+            // errors and messages from the server
-  //           errors: messages
+            errors: messages
-  //         } as ProofStep)
+          } as ProofStep)
-  //       })
+        })
-  //       // Save the proof to the context
+        // Save the proof to the context
-  //       setProof(tmpProof)
+        setProof(tmpProof)
-  //     }).catch((error) => {console.debug("promise broken")})
+      }).catch((error) => {console.debug("promise broken")})
-  //   }).catch((error) => {console.debug("promise broken")})
+    }).catch((error) => {console.debug("promise broken")})
-  // }, [editor, rpcSess, uri, model])
+  }, [editor, rpcSess, uri, model])
  // Run the command
  const runCommand = React.useCallback(() => {
@@ -209,8 +201,6 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
        forceMoveMarkers: false
      }])
      setTypewriterInput('')
      // Load proof after executing edits
      loadGoals(rpcSess, uri, setProof)
    }
    editor.setPosition(pos)
@@ -222,15 +212,9 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
    }
  }, [typewriterInput])
  /* Load proof on start/switching to typewriter */
  useEffect(() => {
-    loadGoals(rpcSess, uri, setProof)
+    if (proof.length && hasInteractiveErrors(proof[proof.length - 1].errors)) {
-  }, [])
+      setTypewriterInput(proof[proof.length - 1].command)
  /** 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])
@@ -238,9 +222,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
  useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
    if (params.uri == uri) {
      setProcessing(false)
-      //loadGoals(rpcSess, uri, setProof)
+      loadAllGoals()
      // TODO: loadAllGoals()
      if (!hasErrors(params.diagnostics)) {
        //setTypewriterInput("")
        editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
@@ -254,15 +236,6 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
    // 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,
@@ -333,8 +306,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
  useEffect(() => {
    console.debug(`time to update: ${uri} \n ${rpcSess}`)
    console.debug(rpcSess)
-    // console.debug('LOAD ALL GOALS')
+    loadAllGoals()
    // TODO: loadAllGoals()
  }, [rpcSess])
  /** Process the entered command */
@@ -343,8 +315,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
    runCommand()
  }
-  // do not display if the proof is completed (with potential warnings still present)
+  return <div className={`typewriter${hidden ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
  return <div className={`typewriter${proof.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
      <form onSubmit={handleSubmit}>
        <div className="typewriter-input-wrapper">
          <div ref={inputRef} className="typewriter-input" />
@@ -372,14 +343,3 @@ export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) {
    (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)
  }
 }
@@ -28,10 +28,10 @@ import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
-  ProofContext, SelectionContext, WorldLevelIdContext } from './infoview/context'
+  ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
-import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api'
+import { GameHint } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints, MoreHelpButton, filterHints } from './hints'
+import { DeletedHints, Hint, Hints, filterHints } from './hints'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import path from 'path';
@@ -49,7 +49,6 @@ import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc'
 import { IConnectionProvider } from 'monaco-languageclient'
 import { monacoSetup } from 'lean4web/client/src/monacoSetup'
 import { onigasmH } from 'onigasm/lib/onigasmH'
 import { isLastStepWithErrors, lastStepHasErrors } from './infoview/goals'
 monacoSetup()
@@ -73,7 +72,7 @@ function Level() {
  </WorldLevelIdContext.Provider>
 }
-function ChatPanel({lastLevel, visible = true}) {
+function ChatPanel({lastLevel}) {
  const chatRef = useRef<HTMLDivElement>(null)
  const {mobile} = useContext(PreferencesContext)
  const gameId = useContext(GameIdContext)
@@ -84,7 +83,9 @@ function ChatPanel({lastLevel, visible = true}) {
  const {selectedStep, setSelectedStep} = useContext(SelectionContext)
  const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
-  let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)
+  // If the last step has errors, we want to treat it as if it is part of the second-to-last step
  let k = proof.length - 1
  let withErr = hasInteractiveErrors(proof[k]?.errors) ? 1 : 0
  function toggleSelection(line: number) {
    return (ev) => {
@@ -97,6 +98,29 @@ function ChatPanel({lastLevel, visible = true}) {
    }
  }
  function hasHiddenHints(i : number): boolean {
    let step = proof[i]
    // For example if the proof isn't loaded yet
    if(!step) {return false}
    return step.hints.some((hint) => hint.hidden)
  }
  const activateHiddenHints = (ev) => {
    // If the last step (`k`) has errors, we want the hidden hints from the
    // second-to-last step to be affected
    if (!(proof.length)) {return}
    // state must not be mutated, therefore we need to clone the set
    let tmp = new Set(showHelp)
    if (tmp.has(k - withErr)) {
      tmp.delete(k - withErr)
    } else {
      tmp.add(k - withErr)
    }
    setShowHelp(tmp)
    console.debug(`help: ${Array.from(tmp.values())}`)
  }
  useEffect(() => {
    // TODO: For some reason this is always called twice
    console.debug('scroll chat')
@@ -122,34 +146,29 @@ function ChatPanel({lastLevel, visible = true}) {
  let introText: Array<string> = level?.data?.introduction.split(/\n(\s*\n)+/)
-  return <div className={`chat-panel ${visible ? '' : 'hidden'}`}>
+  // experimental: Remove all hints that appeared identically in the previous step
  // This effectively prevent consequtive hints being shown.
  let modifiedHints : GameHint[][] = filterHints(proof)
  return <div className="chat-panel">
    <div ref={chatRef} className="chat">
      {introText?.filter(t => t.trim()).map(((t, i) =>
        // Show the level's intro text as hints, too
        <Hint key={`intro-p-${i}`}
          hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
      ))}
-      {proof.steps.map((step, i) => {
+      {modifiedHints.map((step, i) => {
        let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
        if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) {
          return <Hints key={`hints-${i}`}
          hints={filteredHints} showHidden={showHelp.has(i)} step={i}
          selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
        }
      })}
      {/* {modifiedHints.map((step, i) => {
        // It the last step has errors, it will have the same hints
        // as the second-to-last step. Therefore we should not display them.
-        if (!(i == proof.steps.length - 1 && withErr)) {
+        if (!(i == proof.length - 1 && withErr)) {
          // TODO: Should not use index as key.
          return <Hints key={`hints-${i}`}
            hints={step} showHidden={showHelp.has(i)} step={i}
-            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
+            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.length - 1}/>
        }
-      })} */}
+      })}
      <DeletedHints hints={deletedChat}/>
-      {proof.completed &&
+      {completed &&
        <>
          <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
            Level completed! 🎉
@@ -163,7 +182,7 @@ function ChatPanel({lastLevel, visible = true}) {
      }
    </div>
    <div className="button-row">
-      {proof.completed && (lastLevel ?
+      {completed && (lastLevel ?
        <Button to={`/${gameId}`}>
          <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
        </Button> :
@@ -171,13 +190,16 @@ function ChatPanel({lastLevel, visible = true}) {
          Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
        </Button>)
        }
-      <MoreHelpButton />
+      {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
        <Button to="" onClick={activateHiddenHints}>
          Show more help!
        </Button>
      }
    </div>
  </div>
 }
-
+function ExercisePanel({codeviewRef, visible=true}) {
 function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject<HTMLDivElement>, visible?: boolean}) {
  const gameId = React.useContext(GameIdContext)
  const {worldId, levelId} = useContext(WorldLevelIdContext)
  const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -207,7 +229,7 @@ function PlayableLevel({impressum, setImpressum}) {
  const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
  // The state variables for the `ProofContext`
-  const [proof, setProof] = useState<ProofState>({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
+  const [proof, setProof] = useState<Array<ProofStep>>([])
  // When deleting the proof, we want to keep to old messages around until
  // a new proof has been entered. e.g. to consult messages coming from dead ends
  const [deletedChat, setDeletedChat] = useState<Array<GameHint>>([])
@@ -334,15 +356,15 @@ function PlayableLevel({impressum, setImpressum}) {
  useEffect(() => {
    // Forget whether hidden hints are displayed for steps that don't exist yet
-    if (proof.steps.length) {
+    if (proof.length) {
      console.debug(Array.from(showHelp))
-      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.steps.length))))
+      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.length))))
    }
  }, [proof])
  // save showed help in store
  useEffect(() => {
-    if (proof.steps.length) {
+    if (proof.length) {
      console.debug(`showHelp:\n ${showHelp}`)
      dispatch(helpEdited({game: gameId, world: worldId, level: levelId, help: Array.from(showHelp)}))
    }
@@ -600,9 +622,7 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
    }
    // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
    setInfoProvider(infoProvider)
-
+    client.restart()
    // TODO: it looks like we get errors "File Changed" here.
    client.restart("Lean4Game")
    const editorApi = infoProvider.getApi()
@@ -188,18 +188,6 @@
  flex-direction: row;
 }
 .exercise .failed-command {
  background-color: #eee;
  padding: .5em;
  border-radius: .2em;
  /* TODO: It seems my browsers merge the margings of the proof steps,
  so that it only shows once 0.5rem instead of twice. Thus have 1.5 here now.
  */
  margin-bottom: 1.5rem;
  display: flex;
  flex-direction: row;
 }
 .exercise .command-text {
  flex: 1;
  background-color: #fff;
@@ -368,8 +368,3 @@ td code  {
  min-width: 40px;
  text-align: center;
 }
 /* DEBUG */
 .proof .step {
  border: 2px solid rgb(0, 123, 255);
 }
@@ -2,6 +2,15 @@
 Here are some issues experienced by users.
 - You can reset the lake projects involved (i.e. the `server/` folder here as well as your [game's folder](https://github.com/hhu-adam/GameSkeleton)) with the following commands:
  ```
  cd [THE PROJECT]
  rm -rf .lake/
  lake update -R
  lake build
  ```
  If you experience problems related to Lean or lake, you should first try to reset it this way.
 # VSCode Dev-Container
 * If you don't get the pop-up, you might have disabled them, and you can reenable it by
  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
@@ -3,7 +3,6 @@ import Lean.Server.FileWorker
 import GameServer.Game
 import GameServer.ImportModules
 import GameServer.SaveData
 import GameServer.EnvExtensions
 namespace MyModule
@@ -61,8 +60,8 @@ open Snapshots
 open JsonRpc
 /--
-Game-specific state to be packed on top of the `Server.FileWorker.WorkerState`
+Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState`
-used by the Lean server.
+used by the lean server.
 -/
 structure WorkerState :=
  /--
@@ -85,7 +84,7 @@ structure WorkerState :=
 deriving ToJson, FromJson
 /--
-Pack the our custom `WorkerState` on top of the normal worker monad
+Pack the `GameServer.FileWorker.WorkerState` on top of the normal worker monad
 `Server.FileWorker.WorkerM`.
 -/
 abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM
@@ -103,6 +102,16 @@ def addMessage (info : SourceInfo) (inputCtx : Parser.InputContext)
      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
      data     := s }}
 /-- Deprecated! -/
 def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
    Elab.Command.CommandElabM Unit := do
  modify fun st => { st with
    messages := st.messages.add {
      fileName := inputCtx.fileName
      severity := MessageSeverity.error
      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
      data     := s }}
 -- TODO: use HashSet for allowed tactics?
 /--
 Find all tactics in syntax object that are forbidden according to a
@@ -299,7 +308,7 @@ where
  private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
      (snaps : Array Snapshot) : IO Unit := do
    let trees := snaps.map fun snap => snap.infoTree
-    let references ← findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs
+    let references := findModuleRefs m.text trees (localVars := true)
    let param := { version := m.version, references : LeanIleanInfoParams }
    hOut.writeLspNotification { method, param }
@@ -313,79 +322,6 @@ where
    uri : String
  deriving ToJson, FromJson
 structure GameDiagnostics where
  diagnostics : List Diagnostic
 deriving ToJson, FromJson
 structure GameParams where
  uri : String
  diagnostics : GameDiagnostics
 deriving ToJson, FromJson
 /-- WIP: publish diagnostics, all intermediate goals and if the game is completed. -/
 def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.InitializeParams) (hOut : FS.Stream) :
    IO Unit := do
  -- let text := m.text
  -- -- `snap` is the one snapshot containing the entire proof.
  -- let mut goals : Array <| InteractiveGoalsWithHints := #[]
  -- for pos in text.positions do
  --   let source := text.getLineBefore pos
  --   -- iterate over all newlines in the proof and get the goals and hints at each position
  --   if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? text pos then
  --     pure ()
  --     let goalAtPos : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
  --       fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
  --         -- TODO: What does this function body do?
  --         -- let ciAfter := { ci with mctx := ti.mctxAfter }
  --         let ci := if useAfter then
  --             { ci with mctx := tacticInfo.mctxAfter }
  --           else
  --             { ci with mctx := tacticInfo.mctxBefore }
  --         -- compute the interactive goals
  --         let goalMvars : List MVarId ← ci.runMetaM {} do
  --           return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore
  --         let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
  --           goalMvars.mapM fun goal => do
  --             let hints ← findHints goal m initParams
  --             let interactiveGoal ← goalToInteractive goal
  --             return ⟨interactiveGoal, hints⟩
  --         -- TODO: This code is way old, can it be deleted?
  --         -- compute the goal diff
  --         -- let goals ← ciAfter.runMetaM {} (do
  --         --     try
  --         --       Widget.diffInteractiveGoals useAfter ti goals
  --         --     catch _ =>
  --         --       -- fail silently, since this is just a bonus feature
  --         --       return goals
  --         -- )
  --         return interactiveGoals
  --     let goalAtPos : Array InteractiveGoalWithHints := ⟨goalAtPos.foldl (· ++ ·) []⟩
  --     goals := goals.push ⟨goalAtPos, source⟩
  --   else
  --     -- No goals present
  --     goals := goals.push default
  -- -- Question: Is there a difference between the diags of this snap and the last snap?
  -- -- Should we get the diags from there?
  -- let diag : Array Widget.InteractiveDiagnostic := snap.interactiveDiags.toArray
  -- -- Level is completed if there are no errrors or warnings
  -- let completed : Bool := ¬ diag.any (fun d =>
  --   d.severity? == some .error ∨ d.severity? == some .warning)
  -- let param : ProofState := {
  --   steps := goals,
  --   diagnostics := diag,
  --   completed := completed }
  -- TODO
  let param := { uri := m.uri : GameCompletedParams}
  hOut.writeLspNotification { method := "$/game/publishProofState", param }
  /-- Checks whether game level has been completed and sends a notification to the client -/
  def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
    -- check if there is any error or warning
@@ -395,51 +331,65 @@ def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.Ini
    let param := { uri := m.uri : GameCompletedParams}
    hOut.writeLspNotification { method := "$/game/completed", param }
-  /-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/
+  /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
-  -- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private
+  private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-  private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
+      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams)
-      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) :
+      : AsyncElabM (Option Snapshot) := do
      AsyncElabM (Option Snapshot) := do
    cancelTk.check
    let s ← get
    let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
    if lastSnap.isAtEnd then
      publishGameCompleted m ctx.hOut s.snaps
      publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
      publishProgressDone m ctx.hOut
      -- This will overwrite existing ilean info for the file, in case something
      -- went wrong during the incremental updates.
      publishIleanInfoFinal m ctx.hOut s.snaps
      return none
    publishProgressAtPos m lastSnap.endPos ctx.hOut
    -- (modified part)
    -- Make sure that there is at least one snap after the head snap, so that
    -- we can see the current goal even on an empty document
    let couldBeEndSnap := s.snaps.size > 1
    let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
      gameWorkerState initParams
    set { s with snaps := s.snaps.push snap }
    -- TODO(MH): check for interrupt with increased precision
    cancelTk.check
-    publishProofState m snap initParams ctx.hOut
+    /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
      while preferring newer versions over old ones. The former is necessary because we do
      not explicitly clear older diagnostics, while the latter is necessary because we do
      not guarantee that diagnostics are emitted in order. Specifically, it may happen that
      we interrupted this elaboration task right at this point and a newer elaboration task
      emits diagnostics, after which we emit old diagnostics because we did not yet detect
      the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
      because we cannot guarantee that no further diagnostics are emitted after clearing
      them. -/
    -- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
    -- because empty diagnostics clear existing error/information squiggles. Therefore we always
    -- want to publish in case there was previously a message at this position.
    publishDiagnostics m snap.diagnostics.toArray ctx.hOut
    publishIleanInfoUpdate m ctx.hOut #[snap]
    return some snap
-  -- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`.
+  /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
-  @[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps]
+  def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
  def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
      (startAfterMs : UInt32) (gameWorkerState : WorkerState)
      : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
    let ctx ← read
    let some headerSnap := snaps[0]? | panic! "empty snapshots"
    if headerSnap.msgLog.hasErrors then
      -- Treat header processing errors as fatal so users aren't swamped with
      -- followup errors
      publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
      publishIleanInfoFinal m ctx.hOut #[headerSnap]
      return AsyncList.ofList [headerSnap]
    else
      -- This will overwrite existing ilean info for the file since this has a
      -- higher version number.
      publishIleanInfoUpdate m ctx.hOut snaps
      return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
        IO.sleep startAfterMs
-        AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 end Elab
@@ -489,7 +439,7 @@ def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
        validSnaps := validSnaps.dropLast
    -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
    -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
-    unfoldCmdSnaps newMeta validSnaps.toArray cancelTk s ctx
+    unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
      (startAfterMs := ctx.initParams.editDelay.toUInt32)
  StateT.lift <| modify fun st => { st with
    doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
@@ -503,12 +453,6 @@ def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
  fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
  fileMap  := default
 /-- `gameDir` and `module` were added.
 TODO: In general this resembles little similarity with the
 original code, and I don't know why...
 -/
 -- @[inherit_doc Lean.Server.FileWorker.compileHeader]
 def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
    (gameDir : String) (module : Name):
    IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
@@ -544,7 +488,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
    let cmdState := Elab.Command.mkState headerEnv {} opts
    let cmdState := { cmdState with infoState := {
      enabled := true
-      trees := #[Elab.InfoTree.context (.commandCtx {
+      trees := #[Elab.InfoTree.context ({
        env     := headerEnv
        fileMap := m.text
        ngen    := { namePrefix := `_worker }
@@ -561,7 +505,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
    let headerSnap := {
      beginPos := 0
      stx := headerStx
-      mpState := {} -- was `headerParserState`
+      mpState := {}
      cmdState := cmdState
      interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
      tacticCache := (← IO.mkRef {})
@@ -569,52 +513,49 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
    publishDiagnostics m headerSnap.diagnostics.toArray hOut
    return (headerSnap, srcSearchPath)
 /-- Copied from `Lean.Server.FileWorker.initializeWorker`. Added `gameDir` and
 `gameWorkerState` arguments and use custom `unfoldCmdSnaps`. -/
 -- @[inherit_doc Lean.Server.FileWorker.initializeWorker]
 def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
    (gameDir : String) (gameWorkerState : WorkerState) : IO (WorkerContext × Server.FileWorker.WorkerState) := do
  let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
  let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-    (gameDir := gameDir) (module := gameWorkerState.levelInfo.module)
+    gameDir gameWorkerState.levelInfo.module
  let cancelTk ← CancelToken.new
-  let ctx := {
+  let ctx :=
-    hIn  := i
+    { hIn  := i
-    hOut := o
+      hOut := o
-    hLog := e
+      hLog := e
-    headerTask
+      headerTask
-    initParams
+      initParams
-    clientHasWidgets
+      clientHasWidgets
-  }
+    }
  let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-    | Except.ok (s, _) => unfoldCmdSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
+    | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
    | Except.error e   => throw (e : ElabTaskError))
  let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
-  return (ctx, {
+  return (ctx,
-    doc                := doc
+  { doc             := doc
-    initHeaderStx      := headerStx
+    initHeaderStx   := headerStx
    currHeaderStx      := headerStx
    importCachingTask? := none
-    pendingRequests    := RBMap.empty
+    pendingRequests := RBMap.empty
-    rpcSessions        := RBMap.empty
+    rpcSessions     := RBMap.empty
  })
 end Initialization
 section NotificationHandling
 /-- Copied from `Lean.Server.FileWorker.handleDidChange` but with our custom `WorkerM` and
 `updateDocument` -/
 -- @[inherit_doc Lean.Server.FileWorker.handleDidChange]
 def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do
  let docId := p.textDocument
  let changes := p.contentChanges
-  let oldDoc := (← StateT.lift get).doc -- needed a lift to our custom `WorkerM`
+  let oldDoc := (← StateT.lift get).doc
-  let newVersion := docId.version?.getD 0
+  let some newVersion ← pure docId.version?
-  if ¬ changes.isEmpty then
+    | throwServerError "Expected version number"
  if newVersion ≤ oldDoc.meta.version then
    -- TODO(WN): This happens on restart sometimes.
    IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
  else if ¬ changes.isEmpty then
    let newDocText := foldDocumentChanges changes oldDoc.meta.text
    -- modification: set the `DependencyBuildMode` from
    -- `oldDoc.meta.dependencyBuildMode` to `.always`
    updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 end NotificationHandling
@@ -650,34 +591,39 @@ end MessageHandling
 section MainLoop
 /--
-The main-loop. Copied from `Lean.Server.FileWorker.mainLoop`. Use custom `WorkerM` as well
+Erase finished tasks if there are no errors.
-as custom `handleNotification`.
+-/
 private def filterFinishedTasks (acc : PendingRequestMap) (id : RequestID)
    (task : Task (Except IO.Error Unit)) : IO PendingRequestMap := do
  if (← hasFinished task) then
    /- Handler tasks are constructed so that the only possible errors here
    are failures of writing a response into the stream. -/
    if let Except.error e := task.get then
      throwServerError s!"Failed responding to request {id}: {e}"
    pure <| acc.erase id
  else pure acc
 /--
 The main-loop.
 -/
 --@[inherit_doc Lean.Server.FileWorker.mainLoop]
 partial def mainLoop : WorkerM Unit := do
  let ctx ← read
  let mut st ← StateT.lift get
  let msg ← ctx.hIn.readLspMessage
-  -- Erase finished tasks if there are no errors.
+  let pendingRequests ← st.pendingRequests.foldM (fun acc id task =>
-  let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
+    filterFinishedTasks acc id task) st.pendingRequests
      : IO PendingRequestMap := do
    if (← hasFinished task) then
      if let Except.error e := task.get then
        throwServerError s!"Failed responding to request {id}: {e}"
      pure <| acc.erase id
    else pure acc
  let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
  st := { st with pendingRequests }
  -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
  for (id, seshRef) in st.rpcSessions do
    let sesh ← seshRef.get
    if (← sesh.hasExpired) then
      st := { st with rpcSessions := st.rpcSessions.erase id }
  set st
  -- Process the RPC-message and restart main-loop.
  match msg with
  | Message.request id "shutdown" none =>
    --added. TODO: why do we need that? Or has it just removed in Lean since when we started?
    ctx.hOut.writeLspResponse ⟨id, Json.null⟩
    mainLoop
  | Message.request id method (some params) =>
@@ -687,7 +633,6 @@ partial def mainLoop : WorkerM Unit := do
  | Message.notification "exit" none =>
    let doc := st.doc
    doc.cancelTk.set
    doc.cmdSnaps.cancel
    return ()
  | Message.notification method (some params) =>
    -- Custom notification handler
@@ -698,15 +643,10 @@ partial def mainLoop : WorkerM Unit := do
 end MainLoop
-/-- Modified from `Lean.Server.FileWorker.initAndRunWorker`.
+
 Added `gameDir` argument, -/
 -- @[inherit_doc Lean.Server.FileWorker.initAndRunWorker]
 def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
  let i ← maybeTee "fwIn.txt" false i
  let o ← maybeTee "fwOut.txt" true o
  -- BIG MODIFICATION
  let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
  o.writeLspResponse {
    id     := initRequest.id
@@ -722,16 +662,16 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
  discard $ i.readLspNotificationAs "initialized" InitializedParams
  let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
  let doc := param.textDocument
-  -- modification: using `.always`
+  /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
    "\n", which should be enough to handle both LF and CRLF correctly.
    This is because LSP always refers to characters by (line, column),
    so if we get the line number correct it shouldn't matter that there
    is a CR there. -/
  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
  let e := e.withPrefix s!"[{param.textDocument.uri}] "
  let _ ← IO.setStderr e
  try
    -- BIG MODIFICATION
    let game ← loadGameData gameDir
    -- TODO: We misuse the `rootUri` field to the gameName
    let rootUri? : Option String := some (toString game.name)
@@ -751,8 +691,6 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
    -- Run the main loop
    let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
      StateT.run (s := gameWorkerState) <| (mainLoop)
    return (0 : UInt32)
  catch e =>
    IO.eprintln e
@@ -765,12 +703,8 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
 /--
 The main function. Simply wrapping `initAndRunWorker`.
 Copied from `Lean.Server.FileWorker.workerMain`. We add `args` as an argument to pass on
 the `gameDir`.
 TODO: The first arg `args[0]` is always expected to be `--server`. We could drop this completely.
 -/
 -- @[inherit_doc Lean.Server.FileWorker.workerMain]
 def workerMain (opts : Options) (args : List String): IO UInt32 := do
  let i ← IO.getStdin
  let o ← IO.getStdout
@@ -778,6 +712,9 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do
  try
    let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
    let exitCode ← initAndRunWorker i o e opts gameDir
    -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit,
    -- but we definitely don't want to do that in the case of the worker processes,
    -- which can produce non-terminating tasks evaluating user code.
    o.flush
    e.flush
    IO.Process.exit exitCode.toUInt8
@@ -1,19 +1,74 @@
-import GameServer.Structures
+/- This file is mostly copied from `Lean/Widget/InteractiveGoal.lean`. -/
-/-!
+import Lean.Widget.InteractiveGoal
 This file is a modified copy of `Lean.Widget.InteractiveGoal`.
-Note that the structures have been moved to `Structures.lean`, but most of the
+/-! Functionality related to tactic-mode and term-mode goals with embedded `CodeWithInfos`. -/
 functions here must be duplicated from `Lean.Widget.InteractiveGoal` in order
 to use the duplicated structures.
 -/
 namespace GameServer
 open Lean Lean.Widget Lean.Server
-- duplicated with custom `InteractiveGoalCore`
+structure GameHint where
-- @[inherit_doc Lean.Widget.InteractiveGoalCore.pretty]
+  text : String
  hidden : Bool
 deriving FromJson, ToJson
 /-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered
 as `h₁ h₂ : α`. We call this a 'hypothesis bundle'. We use `none` instead of `some false` for
 booleans to save space in the json encoding. -/
 structure InteractiveHypothesisBundle where
  /-- The user-friendly name for each hypothesis. -/
  names : Array Name
  /-- The ids for each variable. Should have the same length as `names`. -/
  fvarIds : Array FVarId
  type : CodeWithInfos
  /-- The value, in the case the hypothesis is a `let`-binder. -/
  val? : Option CodeWithInfos := none
  /-- The hypothesis is a typeclass instance. -/
  isInstance? : Option Bool := none
  /-- The hypothesis is a type. -/
  isType? : Option Bool := none
  /-- The hypothesis's type is of type `Prop` -/
  isAssumption? : Option Bool := none
  /-- If true, the hypothesis was not present on the previous tactic state.
  Only present in tactic-mode goals. -/
  isInserted? : Option Bool := none
  /-- If true, the hypothesis will be removed in the next tactic state.
  Only present in tactic-mode goals. -/
  isRemoved? : Option Bool := none
  deriving Inhabited, RpcEncodable
 /-- The shared parts of interactive term-mode and tactic-mode goals. -/
 structure InteractiveGoalCore where
  hyps : Array InteractiveHypothesisBundle
  /-- The target type. -/
  type : CodeWithInfos
  /-- Metavariable context that the goal is well-typed in. -/
  ctx : WithRpcRef Elab.ContextInfo
 /-- An interactive tactic-mode goal. -/
 structure InteractiveGoal extends InteractiveGoalCore where
  /-- The name `foo` in `case foo`, if any. -/
  userName? : Option String
  /-- The symbol to display before the target type. Usually `⊢ ` but `conv` goals use `∣ `
  and it could be extended. -/
  goalPrefix : String
  /-- Identifies the goal (ie with the unique name of the MVar that it is a goal for.) -/
  mvarId : MVarId
  /-- If true, the goal was not present on the previous tactic state. -/
  isInserted? : Option Bool := none
  /-- If true, the goal will be removed on the next tactic state. -/
  isRemoved? : Option Bool := none
  hints : Array GameHint := #[]
  deriving RpcEncodable
 /-- An interactive term-mode goal. -/
 structure InteractiveTermGoal extends InteractiveGoalCore where
  /-- Syntactic range of the term. -/
  range : Lsp.Range
  /-- Information about the term whose type is the term-mode goal. -/
  term : WithRpcRef Elab.TermInfo
  deriving RpcEncodable
 def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
    (goalPrefix : String) : Format := Id.run do
  let indent := 2 -- Use option
@@ -24,7 +79,8 @@ def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option Str
    ret := addLine ret
    let names := hyp.names
        |>.toList
-        |>.filter (· != toString Name.anonymous)
+        |>.filter (not ∘ Name.isAnonymous)
        |>.map toString
        |> " ".intercalate
    match names with
    | "" =>
@@ -41,24 +97,16 @@ where
  addLine (fmt : Format) : Format :=
    if fmt.isNil then fmt else fmt ++ Format.line
 -- duplicated with custom `InteractiveGoal`
 -- @[inherit_doc Lean.Widget.InteractiveGoal.pretty]
 def InteractiveGoal.pretty (g : InteractiveGoal) : Format :=
  g.toInteractiveGoalCore.pretty g.userName? g.goalPrefix
 -- duplicated with custom `InteractiveTermGoal`
 -- @[inherit_doc Lean.Widget.InteractiveTermGoal.pretty]
 def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format :=
  g.toInteractiveGoalCore.pretty none "⊢ "
 -- duplicated with custom `InteractiveGoal`
 -- @[inherit_doc Lean.Widget.InteractiveGoals]
 structure InteractiveGoals where
  goals : Array InteractiveGoal
  deriving RpcEncodable
 -- duplicated with custom `InteractiveGoals`
 -- @[inherit_doc Lean.Widget.InteractiveGoals.append]
 def InteractiveGoals.append (l r : InteractiveGoals) : InteractiveGoals where
  goals := l.goals ++ r.goals
@@ -66,10 +114,9 @@ instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩
 instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
 open Meta in
-- duplicated with custom `InteractiveHypothesisBundle` and therefore added `isAssumption?`
+/-- Extend an array of hypothesis bundles with another bundle. -/
@[inherit_doc Lean.Widget.addInteractiveHypothesisBundle]
 def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
-    (ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) :
+    (ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) :
    MetaM (Array InteractiveHypothesisBundle) := do
  if ids.size == 0 then
    throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle."
@@ -78,12 +125,11 @@ def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
  return hyps.push {
    names
    fvarIds
-    type        := (← ppExprTagged type)
+    type           := (← ppExprTagged type)
-    val?        := (← value?.mapM ppExprTagged)
+    val?           := (← value?.mapM ppExprTagged)
-    isInstance? := if (← isClass? type).isSome then true else none
+    isInstance?    := if (← isClass? type).isSome then true else none
-    isType?     := if (← instantiateMVars type).isSort then true else none
+    isType?        := if (← instantiateMVars type).isSort then true else none
-    -- Added:
+    isAssumption?  := if (← inferType type).isProp then true else none
    isAssumption? := if (← inferType type).isProp then true else none
  }
 open Meta in
@@ -96,15 +142,13 @@ def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α)
  withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl)
 open Meta in
-
+/-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
-- Duplicated from `Lean.Widget.goalToInteractive` with custom structures
+def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM InteractiveGoal := do
@[inherit_doc Lean.Widget.goalToInteractive]
 def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
  let ppAuxDecls := pp.auxDecls.get (← getOptions)
  let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
  let showLetValues := pp.showLetValues.get (← getOptions)
  withGoalCtx mvarId fun lctx mvarDecl => do
-    let pushPending (ids : Array (String × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
+    let pushPending (ids : Array (Name × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
        : MetaM (Array InteractiveHypothesisBundle) :=
      if ids.isEmpty then
        pure hyps
@@ -112,7 +156,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
        match type? with
        | none      => pure hyps
        | some type => addInteractiveHypothesisBundle hyps ids type
-    let mut varNames : Array (String × FVarId) := #[]
+    let mut varNames : Array (Name × FVarId) := #[]
    let mut prevType? : Option Expr := none
    let mut hyps : Array InteractiveHypothesisBundle := #[]
    for localDecl in lctx do
@@ -121,7 +165,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
      else
        match localDecl with
        | LocalDecl.cdecl _index fvarId varName type _ _ =>
-          let varName := toString varName
+          let varName := varName.simpMacroScopes
          let type ← instantiateMVars type
          if prevType? == none || prevType? == some type then
            varNames := varNames.push (varName, fvarId)
@@ -130,7 +174,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
            varNames := #[(varName, fvarId)]
          prevType? := some type
        | LocalDecl.ldecl _index fvarId varName type val _ _ => do
-          let varName := toString varName
+          let varName := varName.simpMacroScopes
          hyps ← pushPending varNames prevType? hyps
          let type ← instantiateMVars type
          let val? ← if showLetValues then pure (some (← instantiateMVars val)) else pure none
@@ -146,10 +190,11 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
    return {
      hyps
      type := goalFmt
-      ctx := ⟨{← Elab.CommandContextInfo.save with }⟩
+      ctx := ⟨← Elab.ContextInfo.save⟩
      userName?
      goalPrefix := getGoalPrefix mvarDecl
      mvarId
      hints
    }
 end GameServer
@@ -1,6 +1,5 @@
 import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
 import Std.Data.Array.Init.Basic
 open Lean
 open Server
@@ -8,6 +7,7 @@ open Widget
 open RequestM
 open Meta
 /-! ## GameGoal -/
 namespace GameServer
@@ -113,10 +113,10 @@ def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pu
 open Meta in
 /-- Find all hints whose trigger matches the current goal -/
-def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
+def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
  goal.withContext do
-    let some level ← getLevelByFileName? initParams m.mkInputContext.fileName
+    let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
-      | throwError "Level not found: {m.mkInputContext.fileName}"
+      | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
    let hints ← level.hints.filterMapM fun hint => do
      openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
        if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
@@ -134,183 +134,18 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
          return none
    return hints
-- TODO: no need to have `RequestM`, just anything where `mut` works
+open RequestM in
-/-- Add custom diagnostics about whether the level is completed. -/
+def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do
 def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : Bool)
    (completedWithWarnings : Bool) (pos : Lsp.Position)
    (startDiags : Array InteractiveDiagnostic := #[]) :
    RequestM <| Array InteractiveDiagnostic := do
  let mut out : Array InteractiveDiagnostic := startDiags
  if goalCount == 0 then
    if completed then
      out := out.push {
        message := .text "level completed! 🎉"
        range := {
          start := pos
          «end» := pos
          }
        severity? := Lsp.DiagnosticSeverity.information }
    else if completedWithWarnings then
      out := out.push {
        message := .text "level completed with warnings… 🎭"
        range := {
          start := pos
          «end» := pos
          }
        severity? := Lsp.DiagnosticSeverity.information }
    else
      pure ()
  else if goalCount < prevGoalCount then
    out := out.push {
      message := .text "intermediate goal solved! 🎉"
      range := {
        start := pos
        «end» := pos
        }
      severity? := Lsp.DiagnosticSeverity.information
    }
  return out
 def filterUnsolvedGoal (a : Array InteractiveDiagnostic) :
    Array InteractiveDiagnostic :=
  a.filter (fun d => match d.message with
  | .append ⟨(.text x) :: _⟩ => x != "unsolved goals"
  | _ => true)
 /-- Request that returns the goals at the end of each line of the tactic proof
 plus the diagnostics (i.e. warnings/errors) for the proof.
 -/
 def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option ProofState)) := do
  let doc ← readDoc
  let rc ← readThe RequestContext
  let text := doc.meta.text
  -- BUG: trimming here is a problem, since the snap might already be evaluated before
  -- the trimming and then the positions don't match anymore :((
  withWaitFindSnap
    doc
    -- TODO (Alex): I couldn't find a good condition to find the correct snap. So we are looking
    -- for the first snap with goals here.
    -- NOTE (Jon): The entire proof is in one snap, so hoped that Position `0` is good enough.
    (fun snap => ¬ (snap.infoTree.goalsAt? doc.meta.text 0).isEmpty)
    (notFoundX := return none)
    fun snap => do
      -- `snap` is the one snapshot containing the entire proof.
      let mut steps : Array <| InteractiveGoalsWithHints := #[]
      -- Question: Is there a difference between the diags of this snap and the last snap?
      -- Should we get the diags from there?
      -- Answer: The last snap only copied the diags from the end of this snap
      let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray
      -- Level is completed if there are no errrors or warnings
      let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error)
      let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning)
      let mut intermediateGoalCount := 0
      -- only the positions that have non-whitespace characters since the last position
      -- should add a new proof step.
      let positionsWithSource : Array (String.Pos × String) :=
        text.positions.zipWithIndex.filterMap (
          fun (pos, i) => match i with
          | 0 => some (pos, "")
          | i' + 1 =>
            let source : String := Substring.toString ⟨text.source, text.positions.get! i', pos⟩
            if source.trim.length == 0 then
              none
            else
              some (pos, source))
      -- Drop the last position as we ensured that there is always a newline at the end
      for ((pos, source), i) in positionsWithSource.zipWithIndex do
        -- iterate over all steps in the proof and get the goals and hints at each position
        -- diags are labeled in Lsp-positions, which differ from the lean-internal
        -- positions by `1`.
        let lspPosAt := text.utf8PosToLspPos pos
        let mut diagsAtPos : Array InteractiveDiagnostic := filterUnsolvedGoal <|
          -- `+1` for getting the errors after the line.
          match i with
          | 0 =>
            -- `lspPosAt` is `(0, 0)`
            diag.filter (fun d => d.range.start == lspPosAt )
          | i' + 1 =>
            diag.filter (fun d =>
              ((text.utf8PosToLspPos <| (positionsWithSource.get! i').1) ≤ d.range.start) ∧
              d.range.start < lspPosAt )
        if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text pos then
          let goalsAtPos' : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
            fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
              -- TODO: What does this function body do?
              -- let ciAfter := { ci with mctx := ti.mctxAfter }
              let ci := if useAfter then
                  { ci with mctx := tacticInfo.mctxAfter }
                else
                  { ci with mctx := tacticInfo.mctxBefore }
              -- compute the interactive goals
              let goalMvars : List MVarId ← ci.runMetaM {} do
                return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore
              let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
                goalMvars.mapM fun goal => do
                  let hints ← findHints goal doc.meta rc.initParams
                  let interactiveGoal ← goalToInteractive goal
                  return ⟨interactiveGoal, hints⟩
              -- TODO: This code is way old, can it be deleted?
              -- compute the goal diff
              -- let goals ← ciAfter.runMetaM {} (do
              --     try
              --       Widget.diffInteractiveGoals useAfter ti goals
              --     catch _ =>
              --       -- fail silently, since this is just a bonus feature
              --       return goals
              -- )
              return interactiveGoals
          let goalsAtPos : Array InteractiveGoalWithHints := ⟨goalsAtPos'.foldl (· ++ ·) []⟩
          diagsAtPos ← completionDiagnostics goalsAtPos.size intermediateGoalCount
            completed completedWithWarnings lspPosAt diagsAtPos
          intermediateGoalCount := goalsAtPos.size
          steps := steps.push ⟨goalsAtPos, source, diagsAtPos, lspPosAt.line, lspPosAt.character⟩
        else
          -- No goals present
          steps := steps.push ⟨#[], source, diagsAtPos, lspPosAt.line, none⟩
      -- Filter out the "unsolved goals" message
      diag := filterUnsolvedGoal diag
      let lastPos := text.utf8PosToLspPos positionsWithSource.back.1
      let remainingDiags : Array InteractiveDiagnostic :=
        diag.filter (fun d => lastPos ≤ d.range.start)
      return some {
        steps := steps,
        diagnostics := remainingDiags,
        completed := completed,
        completedWithWarnings := completedWithWarnings,
        lastPos := lastPos.line
        }
 open RequestM in
 -- The editor apparently uses this
 def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option <| InteractiveGoals)) := do
  let doc ← readDoc
  -- let rc ← readThe RequestContext
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos p.position
  -- TODO: I couldn't find a good condition to find the correct snap. So we are looking
  -- for the first snap with goals here:
  withWaitFindSnap doc (fun s => ¬ (s.infoTree.goalsAt? doc.meta.text hoverPos).isEmpty)
    (notFoundX := return none) fun snap => do
      if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
-        let goals : List <| Array InteractiveGoal ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+        let goals : List InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
          let ciAfter := { ci with mctx := ti.mctxAfter }
          let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
          -- compute the interactive goals
@@ -318,8 +153,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
            return List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
          let goals ← ci.runMetaM {} do
             goals.mapM fun goal => do
-              -- let hints ← findHints goal doc.meta rc.initParams
+              let hints ← findHints goal doc rc.initParams
-              return ← goalToInteractive goal
+              return ← goalToInteractive goal hints
          -- compute the goal diff
          -- let goals ← ciAfter.runMetaM {} (do
          --     try
@@ -328,8 +163,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
          --       -- fail silently, since this is just a bonus feature
          --       return goals
          -- )
-          return goals
+          return {goals}
-        return some <| ⟨goals.foldl (· ++ ·) #[]⟩
+        return some <| goals.foldl (· ++ ·) ⟨#[]⟩
      else
        return none
@@ -337,16 +172,7 @@ builtin_initialize
  registerBuiltinRpcProcedure
    `Game.getInteractiveGoals
    Lsp.PlainGoalParams
-    (Option <| InteractiveGoals
+    (Option InteractiveGoals)
    )
    getInteractiveGoals
 builtin_initialize
  registerBuiltinRpcProcedure
    `Game.getProofState
    Lsp.PlainGoalParams
    (Option ProofState)
    getProofState
 end GameServer
@@ -1,93 +0,0 @@
 import Lean.Widget.InteractiveGoal
 import Lean.Widget.InteractiveDiagnostic
 import Lean.Data.Lsp.Diagnostics
 /-!
 This file contains the custom data structures use by the server.
 Some of them overwrite built-in structures from Lean.
 In particular, the structures from `Lean.Widget.InteractiveGoal` are duplicated with
 the following extension:
 * `isAssumption?` in `InteractiveHypothesisBundle`: stores if a hypothesis is of type `Prop`.
 NOTE: Changes here need to be reflected in  the corresponding `interface` in `rcp_api.ts`
 on the client-side.
 -/
 open Lean Server Widget
 namespace GameServer
 /-- Extend the interactive hypothesis bundle with an option to distinguish
 "assumptions" from "objects". "Assumptions" are hypotheses of type `Prop`. -/
 -- @[inherit_doc Lean.Widget.InteractiveHypothesisBundle]
 structure InteractiveHypothesisBundle extends Lean.Widget.InteractiveHypothesisBundle where
  /-- The hypothesis's type is of type `Prop` -/
  isAssumption? : Option Bool := none
 deriving RpcEncodable
 -- duplicated but with custom `InteractiveHypothesisBundle`
@[inherit_doc Lean.Widget.InteractiveGoalCore]
 structure InteractiveGoalCore where
  hyps : Array InteractiveHypothesisBundle
  type : CodeWithInfos
  ctx : WithRpcRef Elab.ContextInfo
 -- duplicated but with custom `InteractiveGoalCore`
@[inherit_doc Lean.Widget.InteractiveGoal]
 structure InteractiveGoal extends InteractiveGoalCore where
  userName? : Option String
  goalPrefix : String
  mvarId : MVarId
  isInserted? : Option Bool := none
  isRemoved? : Option Bool := none
 deriving RpcEncodable
 -- duplicated with custom `InteractiveGoalCore`
@[inherit_doc Lean.Widget.InteractiveTermGoal]
 structure InteractiveTermGoal extends InteractiveGoalCore where
  range : Lsp.Range
  term : WithRpcRef Elab.TermInfo
 deriving RpcEncodable
 /-- A hint in the game at the corresponding goal. -/
 structure GameHint where
  text : String
  hidden : Bool
 deriving FromJson, ToJson
 /-- Bundled `InteractiveGoal` together with an array of hints that apply at this stage. -/
 structure InteractiveGoalWithHints where
  goal : InteractiveGoal
  /-- Extended the `InteractiveGoal` by an array of hints at that goal. -/
  hints : Array GameHint
 deriving RpcEncodable
 structure InteractiveGoalsWithHints where
  goals : Array InteractiveGoalWithHints
  /-- The content of the line evaluated. -/
  command : String
  diags : Array InteractiveDiagnostic := default
  line : Option Nat -- only for debugging
  column : Option Nat -- only for debugging
 deriving RpcEncodable
 instance : Inhabited InteractiveGoalsWithHints := ⟨default, default, default, none, none⟩
 /-- Collected goals throughout the proof. Used for communication with the game client. -/
 structure ProofState where
  /-- goals after each line. includes the hints. -/
  steps : Array <| InteractiveGoalsWithHints
  /-- diagnostics contains all errors and warnings.
  TODO: I think they contain information about which line they belong to. Verify this.
  -/
  diagnostics : Array InteractiveDiagnostic := default
  /-- Whether the level is considered solved. -/
  completed : Bool
  completedWithWarnings : Bool
  lastPos : Nat -- only for debugging
 deriving RpcEncodable
@@ -4,10 +4,10 @@
 [{"url": "https://github.com/leanprover/std4.git",
   "type": "git",
   "subDir": null,
-   "rev": "276953b13323ca151939eafaaec9129bf7970306",
+   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
   "name": "std",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0-rc1",
+   "inputRev": "v4.5.0",
   "inherited": false,
   "configFile": "lakefile.lean"}],
 "name": "GameServer",
@@ -8,8 +8,6 @@ def leanVersion : String := s!"v{Lean.versionString}"
 require std from git "https://github.com/leanprover/std4.git" @ leanVersion
 -- require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
 lean_lib GameServer
@[default_target]
@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.5.0
Author	SHA1	Message	Date
Jon Eugster	d689c7ec86	update npm deps	2024-02-23 18:58:15 +01:00
Jon Eugster	16c979a6c2	bump npm dependencies	2024-02-23 18:58:06 +01:00
Jon Eugster	698a88c545	Update troubleshoot.md	2024-02-16 10:57:02 +01:00
`@@ -1 +1 @@`
	`leanprover/lean4:v4.6.0-rc1`	`leanprover/lean4:v4.5.0`