diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx
index 037eb86..10fe55e 100644
--- a/client/src/components/hints.tsx
+++ b/client/src/components/hints.tsx
@@ -1,7 +1,9 @@
-import { GameHint } from "./infoview/rpc_api";
+import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api";
 import * as React from 'react';
 import Markdown from './markdown';
-import { ProofStep } from "./infoview/context";
+import { DeletedChatContext, ProofContext } 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}>
@@ -16,7 +18,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)
 
@@ -46,22 +48,52 @@ export function DeletedHints({hints} : {hints: GameHint[]}) {
 }
 
 /** Filter hints to not show consequtive identical hints twice.
- *
- * 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.
+ * Hidden hints are not filtered.
  */
-export function filterHints(proof: ProofStep[]): GameHint[][] {
-  return proof.map((step, i) => {
-    if (i == 0){
-      return step.hints
+export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
+  if (!hints) {
+    return []}
+  else if (!prevHints) {
+    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() {
+
+  const {proof, setProof} = React.useContext(ProofContext)
+  const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
+
+  let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)
+
+  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 {
-      // 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))
+      tmp.add(k)
     }
-  })
+    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>
+  }
 }
diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts
index e425749..a3d0399 100644
--- a/client/src/components/infoview/context.ts
+++ b/client/src/components/infoview/context.ts
@@ -3,8 +3,8 @@
  */
 import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { InteractiveDiagnostic, InteractiveTermGoal } from '@leanprover/infoview-api';
-import { GameHint, InteractiveGoal, InteractiveGoals } from './rpc_api';
+import { InteractiveDiagnostic } from '@leanprover/infoview-api';
+import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { PreferencesState } from '../../state/preferences';
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
@@ -12,37 +12,39 @@ export const MonacoEditorContext = React.createContext<monaco.editor.IStandalone
 
 export type InfoStatus = 'updating' | 'error' | 'ready';
 
-/** One step of the proof */
-export type ProofStep = {
-  /** The command in this step */
-  command : string
-  /** List of goals *after* this command */
-  goals: InteractiveGoal[]     // TODO: Add correct type
-  /** Story relevant messages */
-  hints: GameHint[]        // TODO: Add correct type
-  /** Errors and warnings */
-  errors: InteractiveDiagnostic[]       // TODO: Add correct type
-}
+// /** One step of the proof */
+// export type ProofStep = {
+//   /** The command in this step */
+//   command : string
+//   /** List of goals *after* this command */
+//   goals: InteractiveGoal[]     // TODO: Add correct type
+//   /** Story relevant messages */
+//   hints: GameHint[]        // TODO: Add correct type
+//   /** Errors and warnings */
+//   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 `null` as command
+   * Note that the first step will always have "" as command
    */
-  proof: ProofStep[],
-  setProof: React.Dispatch<React.SetStateAction<Array<ProofStep>>>
+  proof: ProofState,
+  setProof: React.Dispatch<React.SetStateAction<ProofState>>
 }>({
-  proof: [],
-  setProof: () => {} // TODO: implement me
+  proof: {steps: [], diagnostics: [], completed: false},
+  setProof: () => {}
 })
 
+
+// TODO: Do we still need that?
 export interface ProofStateProps {
   // pos: DocumentPosition;
   status: InfoStatus;
   messages: InteractiveDiagnostic[];
-  goals?: InteractiveGoals;
+  goals?: InteractiveGoalsWithHints;
   termGoal?: InteractiveTermGoal;
   error?: string;
   // userWidgets: UserWidgetInstance[];
@@ -50,18 +52,18 @@ export interface ProofStateProps {
   // triggerUpdate: () => Promise<void>;
 }
 
-export const ProofStateContext = React.createContext<{
-  proofState : ProofStateProps,
-  setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
-}>({
-  proofState : {
-    status: 'updating',
-    messages: [],
-    goals: undefined,
-    termGoal: undefined,
-    error: undefined},
-  setProofState: () => {},
-})
+// export const ProofStateContext = React.createContext<{
+//   proofState : ProofStateProps,
+//   setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
+// }>({
+//   proofState : {
+//     status: 'updating',
+//     messages: [],
+//     goals: undefined,
+//     termGoal: undefined,
+//     error: undefined},
+//   setProofState: () => {},
+// })
 
 export interface IPreferencesContext extends PreferencesState{
   mobile: boolean, // The variables that actually control the page 'layout' can only be changed through layout.
diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
index 6e7049b..01f3a2a 100644
--- a/client/src/components/infoview/goals.tsx
+++ b/client/src/components/infoview/goals.tsx
@@ -10,7 +10,10 @@ 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, InteractiveHypothesisBundle } from './rpc_api';
+import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api';
+import { RpcSessionAtPos } from '@leanprover/infoview/*';
+import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
+import { DiagnosticSeverity } from 'vscode-languageserver-protocol';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -39,7 +42,11 @@ function goalToString(g: InteractiveGoal): string {
 }
 
 export function goalsToString(goals: InteractiveGoals): string {
-    return goals.goals.map(goalToString).join('\n\n')
+    return goals.goals.map(g => goalToString(g)).join('\n\n')
+}
+
+export function goalsWithHintsToString(goals: InteractiveGoalsWithHints): string {
+    return goals.goals.map(g => goalToString(g.goal)).join('\n\n')
 }
 
 interface GoalFilterState {
@@ -255,7 +262,7 @@ export const ProofDisplay = React.memo((props : ProofDisplayProps) => {
 })
 
 interface GoalsProps {
-    goals: InteractiveGoals
+    goals: InteractiveGoalsWithHints
     filter: GoalFilterState
 }
 
@@ -264,7 +271,7 @@ export function Goals({ goals, filter }: GoalsProps) {
         return <>No goals</>
     } else {
         return <>
-          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g} filter={filter} />)}
+          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}
         </>
     }
 }
@@ -276,7 +283,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?: InteractiveGoals
+    goals?: InteractiveGoalsWithHints
 }
 
 /**
@@ -291,7 +298,7 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
             data-id="copy-goal-to-comment"
             onClick={e => {
                 e.preventDefault();
-                if (goals) void ec.copyToComment(goalsToString(goals))
+                if (goals) void ec.copyToComment(goalsWithHintsToString(goals))
             }}
             title="copy state to comment" />
 
@@ -336,3 +343,112 @@ 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)
+}
diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx
index 27f4644..f542a3c 100644
--- a/client/src/components/infoview/info.tsx
+++ b/client/src/components/infoview/info.tsx
@@ -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, InteractiveTermGoal } from '@leanprover/infoview-api'
+  RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api'
 import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound,
   mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util'
 import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'
@@ -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 { InteractiveGoals } from './rpc_api'
+import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } 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>
-  proof? : string
+  proofString? : string
 }
 
 const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
-    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proof} = props
+    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props
 
     const hasWidget = userWidgets.length > 0
     const hasError = !!error
@@ -114,7 +114,8 @@ 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}.
@@ -129,7 +130,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
           </div>
           <div>
             { goals && (goals.goals.length > 0
-              ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
+              ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals[0]?.goal} showHints={true} />
               : <div className="goals-section-title">No Goals</div>
             )}
           </div>
@@ -137,7 +138,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.map (goal => goal) : []}
+            <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []}
               termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
           </details>
         )}
@@ -166,6 +167,7 @@ interface InfoDisplayProps {
   pos: DocumentPosition,
   status: InfoStatus,
   messages: InteractiveDiagnostic[],
+  proof?: ProofState,
   goals?: InteractiveGoals,
   termGoal?: InteractiveTermGoal,
   error?: string,
@@ -175,7 +177,7 @@ interface InfoDisplayProps {
 }
 
 /** Displays goal state and messages. Can be paused. */
-function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable) {
+function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
     // Used to update the paused state *just once* if it is paused,
     // but a display update is triggered
     const [shouldRefresh, setShouldRefresh] = React.useState<boolean>(false)
@@ -214,7 +216,7 @@ function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable)
     {/* <details open> */}
         {/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */}
         <div className="vscode-light">
-            <InfoDisplayContent {...props} proof={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
+            <InfoDisplayContent {...props} proofString={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
         </div>
     {/* </details> */}
     </RpcContext.Provider>
@@ -290,6 +292,8 @@ 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)
@@ -308,6 +312,7 @@ function InfoAux(props: InfoProps) {
                 pos,
                 status: 'updating',
                 messages: lspDiagsHere.map(lspDiagToInteractive),
+                proof: undefined,
                 goals: undefined,
                 termGoal: undefined,
                 error: undefined,
@@ -318,11 +323,12 @@ 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([goalsReq, termGoalReq, widgetsReq, messagesReq]).then(
-            ([goals, termGoal, userWidgets, messages]) => resolve({
+        Promise.all([proofReq, goalsReq, termGoalReq, widgetsReq, messagesReq]).then(
+            ([proof, goals, termGoal, userWidgets, messages]) => resolve({
                 pos,
                 status: 'ready',
                 messages,
+                proof : proof as any,
                 goals: goals as any,
                 termGoal,
                 error: undefined,
@@ -353,6 +359,7 @@ function InfoAux(props: InfoProps) {
                     pos,
                     status: 'error',
                     messages: lspDiagsHere.map(lspDiagToInteractive),
+                    proof: undefined,
                     goals: undefined,
                     termGoal: undefined,
                     error: `Error fetching goals: ${errorString}`,
@@ -389,6 +396,7 @@ function InfoAux(props: InfoProps) {
         pos,
         status: 'updating',
         messages: [],
+        proof: undefined,
         goals: undefined,
         termGoal: undefined,
         error: undefined,
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index 956d2f6..3e768fa 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -26,15 +26,16 @@ import Markdown from '../markdown';
 
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
-import { Goal } from './goals';
-import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
-import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter';
+import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals';
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context';
+import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
-import { GameHint } from './rpc_api';
+import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { store } from '../../state/store';
-import { Hints, filterHints } from '../hints';
+import { Hints, MoreHelpButton, 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.
@@ -61,36 +62,35 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
   const gameId = React.useContext(GameIdContext)
   const { typewriterMode } = React.useContext(InputModeContext)
 
-  // Mark level as completed when server gives notification
+  const {proof, setProof} = React.useContext(ProofContext)
+
   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 }))
-
-        // On completion, add the names of all new items to the local storage
-        let newTiles = [
-          ...level?.tactics,
-          ...level?.lemmas,
-          ...level?.definitions
-        ].filter((tile) => tile.new).map((tile) => tile.name)
-
-        // Add the proven statement to the local storage as well.
-        if (level?.statementName != null) {
-          newTiles.push(level?.statementName)
-        }
 
-        let inv: string[] = selectInventory(gameId)(store.getState())
+  React.useEffect(() => {
+    if (proof.completed) {
+      dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
+
+      // On completion, add the names of all new items to the local storage
+      let newTiles = [
+        ...level?.tactics,
+        ...level?.lemmas,
+        ...level?.definitions
+      ].filter((tile) => tile.new).map((tile) => tile.name)
+
+      // Add the proven statement to the local storage as well.
+      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)
+      let inv: string[] = selectInventory(gameId)(store.getState())
 
-        dispatch(changedInventory({ game: gameId, inventory: newInv }))
-      }
-    }, [level]
-  )
+      // 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,7 +154,7 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
 
-  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
+  const { proof, setProof } = React.useContext(ProofContext)
 
   console.debug(`template: ${props.data?.template}`)
 
@@ -206,7 +206,7 @@ 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">
-      {completed && <div className="level-completed">Level completed! 🎉</div>}
+      {proof.completed && <div className="level-completed">Level completed! 🎉</div>}
       <Infos />
     </div>
   }
@@ -223,15 +223,24 @@ const goalFilter = {
 }
 
 /** The display of a single entered lean command */
-function Command({ command, deleteProof }: { command: string, deleteProof: any }) {
+function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) {
   // The first step will always have an empty command
-  if (!command) { return <></> }
-  return <div className="command">
-    <div className="command-text">{command}</div>
-    <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
-      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
-    </Button>
-  </div>
+  if (!proof?.steps[i]?.command) { return <></> }
+
+  if (isLastStepWithErrors(proof, i)) {
+    // If the last step has errors, we display the command in a different style
+    // indicating that it will be removed on the next try.
+    return <div className="failed-command">
+      <i>Failed command</i>: {proof.steps[i].command}
+    </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) => {
@@ -286,10 +295,14 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 // }, 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: ProofStep, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
+function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, 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) => (
@@ -300,7 +313,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 typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]?.goal} />
     </div>
   </div>
 }
@@ -350,12 +363,11 @@ 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 } = React.useContext(ProofContext)
+  const { proof, setProof } = 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);
 
@@ -367,9 +379,11 @@ export function TypewriterInterface({props}) {
   function deleteProof(line: number) {
     return (ev) => {
       let deletedChat: Array<GameHint> = []
-      filterHints(proof).slice(line).map((hintsAtStep, i) => {
+      proof.steps.slice(line).map((step, i) => {
+        let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
+
         // Only add these hidden hints to the deletion stack which were visible
-        deletedChat = [...deletedChat, ...hintsAtStep.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+        deletedChat = [...deletedChat, ...filteredHints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
       })
       setDeletedChat(deletedChat)
 
@@ -382,7 +396,9 @@ export function TypewriterInterface({props}) {
         forceMoveMarkers: false
       }])
       setSelectedStep(undefined)
-      setTypewriterInput(proof[line].command)
+      setTypewriterInput(proof.steps[line].command)
+      // Reload proof on deleting
+      loadGoals(rpcSess, uri, setProof)
       ev.stopPropagation()
     }
   }
@@ -402,7 +418,7 @@ export function TypewriterInterface({props}) {
 
    // Scroll to the end of the proof if it is updated.
    React.useEffect(() => {
-    if (proof?.length > 1) {
+    if (proof.steps.length > 1) {
       proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
     } else {
       proofPanelRef.current?.scrollTo(0,0)
@@ -423,38 +439,8 @@ export function TypewriterInterface({props}) {
     }
   }, [selectedStep])
 
-  // TODO: This about hidden hints is all copied from `level.tsx`. Can we move that into `hints.tsx`?
-
-  // 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
+  // TODO: superfluous, can be replaced with `withErr` from above
+  let lastStepErrors = proof.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof.steps.length)) : false
 
 
   useServerNotificationEffect("$/game/loading", (params : any) => {
@@ -474,20 +460,22 @@ export function TypewriterInterface({props}) {
       </div>
       <div className='proof' ref={proofPanelRef}>
         <ExerciseStatement data={props.data} />
-        {proof.length ?
+        {proof.steps.length ?
           <>
-            {proof.map((step, i) => {
-              if (i == proof.length - 1 && lastStepErrors) {
-                // if the last command contains an error, we only display the errors but not the
-                // entered command as it is still present in the command line.
-                // TODO: Should not use index as key.
-                return <div key={`proof-step-${i}`}>
-                  <Errors errors={step.errors} typewriterMode={true} />
-                </div>
-              } else {
+            {proof.steps.map((step, i) => {
+              let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
+
+              // if (i == proof.steps.length - 1 && hasInteractiveErrors(step.diags)) {
+              //   // if the last command contains an error, we only display the errors but not the
+              //   // entered command as it is still present in the command line.
+              //   // TODO: Should not use index as key.
+              //   return <div key={`proof-step-${i}`} className={`step step-${i}`}>
+              //     <Errors errors={step.diags} typewriterMode={true} />
+              //   </div>
+              // } else {
                 return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
-                  <Command command={step.command} deleteProof={deleteProof(i)} />
-                  <Errors errors={step.errors} typewriterMode={true} />
+                  <Command proof={proof} i={i} deleteProof={deleteProof(i)} />
+                  <Errors errors={step.diags} 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>
@@ -495,22 +483,21 @@ export function TypewriterInterface({props}) {
                   }
                   {mobile &&
                     <Hints key={`hints-${i}`}
-                      hints={step.hints} showHidden={showHelp.has(i)} step={i}
+                      hints={filteredHints} showHidden={showHelp.has(i)} step={i}
                       selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
                   }
-                  <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
-
-                  {mobile && i == proof.length - 1 &&
-                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
-                      Show more help!
-                    </Button>
+                  {/* <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) => {}}/> */}
+                  {!(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.steps.length - 1 &&
+                    <MoreHelpButton />
                   }
 
                   {/* Show a message that there are no goals left */}
-                  {!step.goals.length && (
+                  {/* {!step.goals.length && (
                     <div className="message information">
-                      {completed ?
+                      {proof.completed ?
                         <p>Level completed! 🎉</p> :
                         <p>
                           <b>no goals left</b><br />
@@ -518,11 +505,17 @@ 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}`}>
@@ -539,7 +532,7 @@ export function TypewriterInterface({props}) {
         }
       </div>
     </div>
-    <Typewriter hidden={!withErr && proof[proof.length - 1]?.goals.length == 0} disabled={disableInput || !proof.length}/>
+    <Typewriter disabled={disableInput || !proof.steps.length}/>
     </RpcContext.Provider>
   </div>
 }
diff --git a/client/src/components/infoview/rpc_api.ts b/client/src/components/infoview/rpc_api.ts
index 3833c61..c499e93 100644
--- a/client/src/components/infoview/rpc_api.ts
+++ b/client/src/components/infoview/rpc_api.ts
@@ -3,46 +3,80 @@
  *
  * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts`
  */
-import { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
-
-export interface GameHint {
-  text: string;
-  hidden: boolean;
-}
+import type { Range } from 'vscode-languageserver-protocol';
+import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
+import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*';
+import type { 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[];
-  /** Present since server version 1.1.2. */
   fvarIds?: FVarId[];
   type: CodeWithInfos;
   val?: CodeWithInfos;
   isInstance?: boolean;
   isType?: boolean;
-  isAssumption?: boolean;
   isInserted?: boolean;
   isRemoved?: boolean;
+  isAssumption?: 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;
+}
+
+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 {
+  goal: InteractiveGoal;
   hints: GameHint[];
 }
 
-export interface InteractiveGoals {
-  goals: InteractiveGoal[];
+export interface InteractiveGoalsWithHints {
+  goals: InteractiveGoalWithHints[];
+  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;
 }
diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx
index 347a021..e457af0 100644
--- a/client/src/components/infoview/typewriter.tsx
+++ b/client/src/components/infoview/typewriter.tsx
@@ -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 } from 'vscode-languageserver-protocol';
+import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol';
 import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
@@ -13,13 +13,21 @@ 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, getInteractiveDiagnostics } from '@leanprover/infoview-api';
+import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } from '@leanprover/infoview-api';
 import { Diagnostic } from 'vscode-languageserver-types';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
-import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context'
-import { goalsToString } from './goals'
-import { GameHint, InteractiveGoals } from './rpc_api'
+import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext } from './context'
+import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
+import { GameHint, ProofState } 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. */
 
@@ -64,7 +72,7 @@ config.autoClosingPairs = config.autoClosingPairs.map(
 monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 /** The input field */
-export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boolean}) {
+export function Typewriter({disabled}: {disabled?: boolean}) {
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
@@ -89,98 +97,98 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   /** Load all goals an messages of the current proof (line-by-line) and save
    * the retrieved information into context (`ProofContext`)
    */
-  const loadAllGoals = React.useCallback(() => {
-
-    let goalCalls = []
-    let msgCalls = []
-
-    // For each line of code ask the server for the goals and the messages on this line
-    for (let i = 0; i < model.getLineCount(); i++) {
-      goalCalls.push(
-        rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
-      )
-      msgCalls.push(
-        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
-    Promise.all(goalCalls).then((steps : InteractiveGoals[]) => {
-      Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
-        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.goals.length && goalCount > goals.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.goals.length
-
-          // with no goals there will be no hints.
-          let hints : GameHint[] = goals.goals.length ? goals.goals[0].hints : []
-
-          console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
-          console.debug(`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.goals,
-            // 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)
-      }).catch((error) => {console.debug("promise broken")})
-    }).catch((error) => {console.debug("promise broken")})
-  }, [editor, rpcSess, uri, model])
+  // const loadAllGoals = React.useCallback(() => {
+
+  //   let goalCalls = []
+  //   let msgCalls = []
+
+  //   // For each line of code ask the server for the goals and the messages on this line
+  //   for (let i = 0; i < model.getLineCount(); i++) {
+  //     goalCalls.push(
+  //       rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
+  //     )
+  //     msgCalls.push(
+  //       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
+  //   Promise.all(goalCalls).then((steps : InteractiveGoalsWithHints[]) => {
+  //     Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
+  //       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)
+  //     }).catch((error) => {console.debug("promise broken")})
+  //   }).catch((error) => {console.debug("promise broken")})
+  // }, [editor, rpcSess, uri, model])
 
   // Run the command
   const runCommand = React.useCallback(() => {
@@ -201,6 +209,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
         forceMoveMarkers: false
       }])
       setTypewriterInput('')
+      // Load proof after executing edits
+      loadGoals(rpcSess, uri, setProof)
     }
 
     editor.setPosition(pos)
@@ -212,9 +222,15 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     }
   }, [typewriterInput])
 
+  /* Load proof on start/switching to typewriter */
+  useEffect(() => {
+    loadGoals(rpcSess, uri, setProof)
+  }, [])
+
+  /** If the last step has an error, add the command to the typewriter. */
   useEffect(() => {
-    if (proof.length && hasInteractiveErrors(proof[proof.length - 1].errors)) {
-      setTypewriterInput(proof[proof.length - 1].command)
+    if (lastStepHasErrors(proof)) {
+      setTypewriterInput(proof.steps[proof.steps.length - 1].command)
     }
   }, [proof])
 
@@ -222,7 +238,9 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == uri) {
       setProcessing(false)
-      loadAllGoals()
+      //loadGoals(rpcSess, uri, setProof)
+
+      // TODO: loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
         //setTypewriterInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
@@ -236,6 +254,15 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     // 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,
@@ -306,7 +333,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   useEffect(() => {
     console.debug(`time to update: ${uri} \n ${rpcSess}`)
     console.debug(rpcSess)
-    loadAllGoals()
+    // console.debug('LOAD ALL GOALS')
+    // TODO: loadAllGoals()
   }, [rpcSess])
 
   /** Process the entered command */
@@ -315,7 +343,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     runCommand()
   }
 
-  return <div className={`typewriter${hidden ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
+  // do not display if the proof is completed (with potential warnings still present)
+  return <div className={`typewriter${proof.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
       <form onSubmit={handleSubmit}>
         <div className="typewriter-input-wrapper">
           <div ref={inputRef} className="typewriter-input" />
@@ -343,3 +372,14 @@ 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)
+  }
+}
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index dbd62a5..beaf30b 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -28,10 +28,10 @@ import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
-  ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
+  ProofContext, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
-import { GameHint } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints, filterHints } from './hints'
+import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api'
+import { DeletedHints, Hint, Hints, MoreHelpButton, filterHints } from './hints'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import path from 'path';
 
@@ -49,6 +49,7 @@ 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()
@@ -83,9 +84,7 @@ function ChatPanel({lastLevel}) {
   const {selectedStep, setSelectedStep} = useContext(SelectionContext)
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
 
-  // 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
+  let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)
 
   function toggleSelection(line: number) {
     return (ev) => {
@@ -98,29 +97,6 @@ function ChatPanel({lastLevel}) {
     }
   }
 
-  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')
@@ -146,10 +122,6 @@ function ChatPanel({lastLevel}) {
 
   let introText: Array<string> = level?.data?.introduction.split(/\n(\s*\n)+/)
 
-  // 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) =>
@@ -157,18 +129,27 @@ function ChatPanel({lastLevel}) {
         <Hint key={`intro-p-${i}`}
           hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
       ))}
-      {modifiedHints.map((step, i) => {
+      {proof.steps.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.length - 1 && withErr)) {
+        if (!(i == proof.steps.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.length - 1}/>
+            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
         }
-      })}
+      })} */}
       <DeletedHints hints={deletedChat}/>
-      {completed &&
+      {proof.completed &&
         <>
           <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
             Level completed! 🎉
@@ -182,7 +163,7 @@ function ChatPanel({lastLevel}) {
       }
     </div>
     <div className="button-row">
-      {completed && (lastLevel ?
+      {proof.completed && (lastLevel ?
         <Button to={`/${gameId}`}>
           <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
         </Button> :
@@ -190,15 +171,12 @@ function ChatPanel({lastLevel}) {
           Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
         </Button>)
         }
-      {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-        <Button to="" onClick={activateHiddenHints}>
-          Show more help!
-        </Button>
-      }
+      <MoreHelpButton />
     </div>
   </div>
 }
 
+
 function ExercisePanel({codeviewRef, visible=true}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
@@ -229,7 +207,7 @@ function PlayableLevel({impressum, setImpressum}) {
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
   // The state variables for the `ProofContext`
-  const [proof, setProof] = useState<Array<ProofStep>>([])
+  const [proof, setProof] = useState<ProofState>({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
   // 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>>([])
@@ -356,15 +334,15 @@ function PlayableLevel({impressum, setImpressum}) {
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
-    if (proof.length) {
+    if (proof.steps.length) {
       console.debug(Array.from(showHelp))
-      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.length))))
+      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.steps.length))))
     }
   }, [proof])
 
   // save showed help in store
   useEffect(() => {
-    if (proof.length) {
+    if (proof.steps.length) {
       console.debug(`showHelp:\n ${showHelp}`)
       dispatch(helpEdited({game: gameId, world: worldId, level: levelId, help: Array.from(showHelp)}))
     }
@@ -622,6 +600,8 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
     }
     // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
     setInfoProvider(infoProvider)
+
+    // TODO: it looks like we get errors "File Changed" here.
     client.restart()
 
     const editorApi = infoProvider.getApi()
diff --git a/client/src/css/infoview.css b/client/src/css/infoview.css
index cab47e8..0a786c4 100644
--- a/client/src/css/infoview.css
+++ b/client/src/css/infoview.css
@@ -188,6 +188,18 @@
   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;
diff --git a/client/src/css/level.css b/client/src/css/level.css
index 82058d3..ff96f7f 100644
--- a/client/src/css/level.css
+++ b/client/src/css/level.css
@@ -368,3 +368,8 @@ td code  {
   min-width: 40px;
   text-align: center;
 }
+
+/* DEBUG */
+.proof .step {
+  border: 2px solid rgb(0, 123, 255);
+}
diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean
index ea9878b..a63b5e1 100644
--- a/server/GameServer/FileWorker.lean
+++ b/server/GameServer/FileWorker.lean
@@ -3,6 +3,7 @@ import Lean.Server.FileWorker
 import GameServer.Game
 import GameServer.ImportModules
 import GameServer.SaveData
+import GameServer.EnvExtensions
 
 namespace MyModule
 
@@ -60,8 +61,8 @@ open Snapshots
 open JsonRpc
 
 /--
-Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState`
-used by the lean server.
+Game-specific state to be packed on top of the `Server.FileWorker.WorkerState`
+used by the Lean server.
 -/
 structure WorkerState :=
   /--
@@ -84,7 +85,7 @@ structure WorkerState :=
 deriving ToJson, FromJson
 
 /--
-Pack the `GameServer.FileWorker.WorkerState` on top of the normal worker monad
+Pack the our custom `WorkerState` on top of the normal worker monad
 `Server.FileWorker.WorkerM`.
 -/
 abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM
@@ -102,16 +103,6 @@ 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
@@ -322,6 +313,79 @@ 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
@@ -331,65 +395,51 @@ where
     let param := { uri := m.uri : GameCompletedParams}
     hOut.writeLspNotification { method := "$/game/completed", param }
 
-  /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
-  private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams)
-      : AsyncElabM (Option Snapshot) := do
+  /-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/
+  -- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private
+  private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
+      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) :
+      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
-    /- 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.
+    publishProofState m snap initParams ctx.hOut
     publishDiagnostics m snap.diagnostics.toArray ctx.hOut
     publishIleanInfoUpdate m ctx.hOut #[snap]
     return some snap
 
-  /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
-  def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
+  -- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`.
+  @[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps]
+  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 (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 
 end Elab
 
@@ -439,7 +489,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)
-    unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
+    unfoldCmdSnaps 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 }}
@@ -513,49 +563,52 @@ 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 gameWorkerState.levelInfo.module
+    (gameDir := gameDir) (module := gameWorkerState.levelInfo.module)
   let cancelTk ← CancelToken.new
-  let ctx :=
-    { hIn  := i
-      hOut := o
-      hLog := e
-      headerTask
-      initParams
-      clientHasWidgets
-    }
+  let ctx := {
+    hIn  := i
+    hOut := o
+    hLog := e
+    headerTask
+    initParams
+    clientHasWidgets
+  }
   let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-    | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
+    | Except.ok (s, _) => unfoldCmdSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
     | Except.error e   => throw (e : ElabTaskError))
   let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
-  return (ctx,
-  { doc             := doc
-    initHeaderStx   := headerStx
+  return (ctx, {
+    doc                := doc
+    initHeaderStx      := headerStx
     currHeaderStx      := headerStx
     importCachingTask? := none
-    pendingRequests := RBMap.empty
-    rpcSessions     := RBMap.empty
+    pendingRequests    := 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
-  let some newVersion ← pure docId.version?
-    | 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 oldDoc := (← StateT.lift get).doc -- needed a lift to our custom `WorkerM`
+  let newVersion := docId.version?.getD 0
+  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
@@ -591,39 +644,34 @@ end MessageHandling
 section MainLoop
 
 /--
-Erase finished tasks if there are no errors.
--/
-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.
+The main-loop. Copied from `Lean.Server.FileWorker.mainLoop`. Use custom `WorkerM` as well
+as custom `handleNotification`.
 -/
+--@[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
-  let pendingRequests ← st.pendingRequests.foldM (fun acc id task =>
-    filterFinishedTasks acc id task) st.pendingRequests
+  -- Erase finished tasks if there are no errors.
+  let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
+      : 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) =>
@@ -633,6 +681,7 @@ 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
@@ -643,10 +692,15 @@ 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
@@ -662,16 +716,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
-  /- 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. -/
+  -- modification: using `.always`
   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)
@@ -691,6 +745,8 @@ 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
@@ -703,8 +759,12 @@ 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
@@ -712,9 +772,6 @@ 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
diff --git a/server/GameServer/InteractiveGoal.lean b/server/GameServer/InteractiveGoal.lean
index ca75ba5..0377f24 100644
--- a/server/GameServer/InteractiveGoal.lean
+++ b/server/GameServer/InteractiveGoal.lean
@@ -1,62 +1,19 @@
-import Lean.Widget.InteractiveGoal
+import GameServer.Structures
 
 /-!
 This file is a modified copy of `Lean.Widget.InteractiveGoal`.
 
-We add the structure `GameHint` and extend two existing structures:
-
-* `isAssumption?` in `InteractiveHypothesisBundle`: stores if a hypothesis is of type `Prop`.
-* `hint` in `InteractiveGoal`: stores the game hints associated with the goal.
-
-The rest of this file is simply copied to use these new modified stuctures.
+Note that the structures have been moved to `Structures.lean`, but most of the
+functions here must be duplicated from `Lean.Widget.InteractiveGoal` in order
+to use the duplicated structures.
 -/
 
 namespace GameServer
 
 open Lean Lean.Widget Lean.Server
 
-/-- A hint in the game at the corresponding goal. -/
-structure GameHint where
-  text : String
-  hidden : Bool
-deriving FromJson, ToJson
-
-/-- Extend the interactive hypothesis bundle with an option to distinguish
-"assumptions" from "objects". "Assumptions" ate hyptheses 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` and extended by `hints`
-@[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
-  /-- Extended the `InteractiveGoal` by an array of hints at that goal. -/
-  hints : Array GameHint := #[]
-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
-
 -- duplicated with custom `InteractiveGoalCore`
-@[inherit_doc Lean.Widget.InteractiveGoalCore.pretty]
+-- @[inherit_doc Lean.Widget.InteractiveGoalCore.pretty]
 def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
     (goalPrefix : String) : Format := Id.run do
   let indent := 2 -- Use option
@@ -140,10 +97,9 @@ def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α)
 
 open Meta in
 
--- Copied from `Lean.Widget.goalToInteractive` but added
--- argument `hint` which is simply passed along.
+-- Duplicated from `Lean.Widget.goalToInteractive` with custom structures
 @[inherit_doc Lean.Widget.goalToInteractive]
-def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM InteractiveGoal := do
+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)
@@ -165,9 +121,6 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
       else
         match localDecl with
         | LocalDecl.cdecl _index fvarId varName type _ _ =>
-          -- We rely on the fact that `withGoalCtx` runs `LocalContext.sanitizeNames`,
-          -- so the `userName`s of local hypotheses are already pretty-printed
-          -- and it suffices to simply `toString` them.
           let varName := toString varName
           let type ← instantiateMVars type
           if prevType? == none || prevType? == some type then
@@ -197,8 +150,6 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
       userName?
       goalPrefix := getGoalPrefix mvarDecl
       mvarId
-      -- Added:
-      hints
     }
 
 end GameServer
diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean
index 1fcdc5e..8069b65 100644
--- a/server/GameServer/RpcHandlers.lean
+++ b/server/GameServer/RpcHandlers.lean
@@ -7,7 +7,6 @@ open Widget
 open RequestM
 open Meta
 
-
 /-! ## GameGoal -/
 
 namespace GameServer
@@ -113,10 +112,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) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
+def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
   goal.withContext do
-    let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
-      | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
+    let some level ← getLevelByFileName? initParams m.mkInputContext.fileName
+      | throwError "Level not found: {m.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,8 +133,212 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams :
           return none
     return hints
 
+/-- Get the line that ends in `pos`. Note that `pos` is expected to be the
+position of a `\n` but this is not enforced. -/
+def _root_.Lean.FileMap.getLineBefore (fmap : FileMap) (pos : String.Pos) : String := Id.run do
+  match fmap.positions.findIdx? (· == pos) with
+  | none =>
+    panic s!"Position {pos} is not a newline character in " ++
+      s!"the following string: '{fmap.source}'!"
+  | some 0 =>
+    -- the first entry of `positions` is always `0`
+    return ""
+  | some (i + 1) =>
+    let line : Substring := ⟨fmap.source, fmap.positions.get! i, pos⟩
+    return line.toString
+
+/-- Returns the `List` without the last element. -/
+def _root_.List.dropBack {α : Type _} : List α → List α
+| [] => []
+| _ :: [] => []
+| x :: xs => x :: xs.dropBack
+
+/-- Trim empty lines from the file and add a single newline. -/
+def _root_.Lean.FileMap.trim (fmap : FileMap) : FileMap :=
+  let str := match fmap.source.trim with
+  | "" => ""
+  | s => s ++ "\n"
+  FileMap.ofString str
+
+/-- Returns the `Array` without the last element. -/
+def _root_.Array.dropBack {α : Type _} (a : Array α) : Array α := ⟨a.data.dropBack⟩
+
+/-- Add custom diagnostics about whether the level is completed. -/
+def addCompletionDiagnostics (diag : Array InteractiveDiagnostic) (goals : Array InteractiveGoalWithHints)
+    (pos : Lsp.Position) (prevGoalCount : Nat) : RequestM <| Array InteractiveDiagnostic := do
+  let mut out : Array InteractiveDiagnostic := diag
+
+  if goals.size == 0 then
+    if diag.any (·.severity? == some .error) then
+      pure ()
+    else if diag.any (·.severity? == some .warning) then
+      out := out.push {
+        message := .text "level completed with warnings. 🎭"
+        range := {
+          start := pos
+          «end» := pos
+          }
+        severity? := Lsp.DiagnosticSeverity.information }
+    else
+      out := out.push {
+        message := .text "level completed! 🎉"
+        range := {
+          start := pos
+          «end» := pos
+          }
+        severity? := Lsp.DiagnosticSeverity.information }
+  else if goals.size < prevGoalCount then
+    out := out.push {
+      message := .text "intermediate goal solved! 🎉"
+      range := {
+        start := pos
+        «end» := pos
+        }
+      severity? := Lsp.DiagnosticSeverity.information
+    }
+
+
+  return out
+          -- diagsAtPos := if goalsAtPos.size < intermediateGoalCount then
+          --   diagsAtPos.push {
+          --     message := .text "intermediate goal solved 🎉"
+          --     range := {
+          --       start := lspPosAt
+          --       «end» := lspPosAt
+          --       }
+          --     severity? := Lsp.DiagnosticSeverity.information
+          --   }
+          --   else diagsAtPos
+
+/-- 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.trim
+
+  -- 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
+
+      let mut intermediateGoalCount := 0
+
+      -- Drop the last position as we ensured that there is always a newline at the end
+      for pos in text.positions.dropBack do
+        -- iterate over all newlines in the proof and get the goals and hints at each position
+        -- TODO: we drop the last position because we always have a newline. Would be better
+        -- to trim newlines instead before submitting!
+        let source := text.getLineBefore pos
+
+        if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? doc.meta.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 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 := ⟨goalAtPos.foldl (· ++ ·) []⟩
+
+          -- 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 :=
+            -- `+1` for getting the errors after the line.
+            diag.filter (·.range.start.line + 1 == lspPosAt.line)
+
+          diagsAtPos ← addCompletionDiagnostics diagsAtPos goalsAtPos lspPosAt intermediateGoalCount
+
+          intermediateGoalCount := goalsAtPos.size
+
+          steps := steps.push ⟨goalsAtPos, source, diagsAtPos, lspPosAt.line, lspPosAt.character⟩
+        else
+          -- No goals present
+          steps := steps.push default
+
+
+
+      --       //   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 🎉'
+      -- //       }
+      -- //     })
+      -- //   }
+
+      -- 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)
+
+      -- Filter out the "unsolved goals" message
+      diag := diag.filter (fun d => match d.message with
+        | .append ⟨(.text x) :: _⟩ => x != "unsolved goals"
+        | _ => true)
+
+      let lastPos := text.utf8PosToLspPos text.positions.back
+      let remainingDiags : Array InteractiveDiagnostic :=
+        diag.filter (fun d => d.range.start.line >= lastPos.line)
+
+      return some {
+        steps := steps,
+        diagnostics := remainingDiags,
+        completed := completed,
+        completedWithWarnings := completedWithWarnings,
+        lastPos := lastPos.line
+        }
+
 open RequestM in
-def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do
+
+def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option <| InteractiveGoals)) := do
   let doc ← readDoc
   let rc ← readThe RequestContext
   let text := doc.meta.text
@@ -145,7 +348,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
   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 InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+        let goals : List <| Array InteractiveGoal ← 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
@@ -153,8 +356,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 rc.initParams
-              return ← goalToInteractive goal hints
+              -- let hints ← findHints goal doc.meta rc.initParams
+              return ← goalToInteractive goal
           -- compute the goal diff
           -- let goals ← ciAfter.runMetaM {} (do
           --     try
@@ -163,8 +366,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
           --       -- fail silently, since this is just a bonus feature
           --       return goals
           -- )
-          return {goals}
-        return some <| goals.foldl (· ++ ·) ⟨#[]⟩
+          return goals
+        return some <| ⟨goals.foldl (· ++ ·) #[]⟩
       else
         return none
 
@@ -172,7 +375,16 @@ builtin_initialize
   registerBuiltinRpcProcedure
     `Game.getInteractiveGoals
     Lsp.PlainGoalParams
-    (Option InteractiveGoals)
+    (Option <| InteractiveGoals
+    )
     getInteractiveGoals
 
+builtin_initialize
+  registerBuiltinRpcProcedure
+    `Game.getProofState
+    Lsp.PlainGoalParams
+    (Option ProofState)
+    getProofState
+
+
 end GameServer
diff --git a/server/GameServer/Structures.lean b/server/GameServer/Structures.lean
new file mode 100644
index 0000000..7b27917
--- /dev/null
+++ b/server/GameServer/Structures.lean
@@ -0,0 +1,93 @@
+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
diff --git a/server/lake-manifest.json b/server/lake-manifest.json
index fce8027..8bf50b9 100644
--- a/server/lake-manifest.json
+++ b/server/lake-manifest.json
@@ -9,6 +9,24 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.5.0",
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "rev": "a6b484980b41aab874fb3113ec5245bd91b625d8",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.4.0",
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",
  "lakeDir": ".lake"}
diff --git a/server/lakefile.lean b/server/lakefile.lean
index fc337ce..a442a32 100644
--- a/server/lakefile.lean
+++ b/server/lakefile.lean
@@ -8,6 +8,8 @@ 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]