show more help per proof step

client/src/components/infoview/command_line.tsx

@@ -19,7 +19,7 @@ import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/in
 import { useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context'
 import { goalsToString } from './goals'
-import { InteractiveGoals } from './rpc_api'
+import { GameHint, InteractiveGoals } from './rpc_api'
 
 /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
 
@@ -155,14 +155,14 @@ export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObj
           }
           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}): `, goals.goals[0]?.hints)
+          console.debug(`Hints: (${i}): `, hints)
           console.debug(`Errors: (${i}): `, messages)
 
-          // with no goals there will be no hints
-          let hints = goals.goals.length ? goals.goals[0].hints : []
-
           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.

client/src/components/infoview/context.ts

@@ -75,9 +75,13 @@ export const SelectionContext = React.createContext<{
 export const DeletedChatContext = React.createContext<{
   deletedChat : GameHint[],
   setDeletedChat: React.Dispatch<React.SetStateAction<Array<GameHint>>>
+  showHelp : Set<number>,
+  setShowHelp: React.Dispatch<React.SetStateAction<Set<number>>>
 }>({
   deletedChat: undefined,
-  setDeletedChat: () => {}
+  setDeletedChat: () => {},
+  showHelp: undefined,
+  setShowHelp: () => {}
 })
 
 export const InputModeContext = React.createContext<{

client/src/components/infoview/main.tsx

@@ -276,7 +276,7 @@ export function CommandLineInterface(props: {world: string, level: number, data:
   const gameId = React.useContext(GameIdContext)
   const {proof} = React.useContext(ProofContext)
   const {selectedStep, setSelectedStep} = React.useContext(SelectionContext)
-  const {setDeletedChat} = React.useContext(DeletedChatContext)
+  const {setDeletedChat, showHelp} = React.useContext(DeletedChatContext)
 
   const proofPanelRef = React.useRef<HTMLDivElement>(null)
 
@@ -305,8 +305,9 @@ export function CommandLineInterface(props: {world: string, level: number, data:
   function deleteProof(line: number) {
     return (ev) => {
       let deletedChat: Array<GameHint> = []
-      proof.slice(line).map(step => {
-        deletedChat = [...deletedChat, ...step.hints]
+      proof.slice(line).map((step, i) => {
+        // Only add these hidden hints to the deletion stack which were visible
+        deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line+i)))]
       })
       setDeletedChat(deletedChat)