fix InfoTree.lean (cf. leanprover/lean4#5835)

REPL/Lean/InfoTree.lean

@@ -53,6 +53,7 @@ namespace Lean.Elab.Info
 def kind : Info → String
   | .ofTacticInfo         _ => "TacticInfo"
   | .ofTermInfo           _ => "TermInfo"
+  | ofPartialTermInfo     _ => "PartialTermInfo"
   | .ofCommandInfo        _ => "CommmandInfo"
   | .ofMacroExpansionInfo _ => "MacroExpansionInfo"
   | .ofOptionInfo         _ => "OptionInfo"
@@ -63,11 +64,13 @@ def kind : Info → String
   | .ofFVarAliasInfo      _ => "FVarAliasInfo"
   | .ofFieldRedeclInfo    _ => "FieldRedeclInfo"
   | .ofOmissionInfo       _ => "OmissionInfo"
+  | .ofChoiceInfo         _ => "ChoiceInfo"
 
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
 def stx? : Info → Option Syntax
   | .ofTacticInfo         info => info.stx
   | .ofTermInfo           info => info.stx
+  | ofPartialTermInfo     info => info.stx
   | .ofCommandInfo        info => info.stx
   | .ofMacroExpansionInfo info => info.stx
   | .ofOptionInfo         info => info.stx
@@ -78,6 +81,7 @@ def stx? : Info → Option Syntax
   | .ofFVarAliasInfo      _    => none
   | .ofFieldRedeclInfo    info => info.stx
   | .ofOmissionInfo       info => info.stx
+  | .ofChoiceInfo         info => info.stx
 
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 def isOriginal (i : Info) : Bool :=
@@ -214,13 +218,13 @@ def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Posit
 
 def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × Position × Position × Array Name) :=
     -- HACK: creating a child ngen
-  t.findTacticNodes.map fun ⟨i, ctx⟩ => 
-    let range := stxRange ctx.fileMap i.stx 
-    ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, 
-      i.stx, 
-      i.goalsBefore, 
-      range.fst, 
-      range.snd, 
+  t.findTacticNodes.map fun ⟨i, ctx⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 },
+      i.stx,
+      i.goalsBefore,
+      range.fst,
+      range.snd,
       i.getUsedConstantsAsSet.toArray )