hints and diags in editor

2024-02-14 15:02:14 +01:00
parent 976d1c6901
commit c0acde14e2
4 changed files with 48 additions and 9 deletions
@@ -68,12 +68,12 @@ function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
 }


-export function MoreHelpButton() {
+export function MoreHelpButton({selected=null} : {selected?: number}) {

  const {proof, setProof} = React.useContext(ProofContext)
  const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)

-  let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)
+  let k = (selected === null) ? (proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected

  const activateHiddenHints = (ev) => {
    // If the last step (`k`) has errors, we want the hidden hints from the