From 5a564bf02bf4feb295dde98ca9311512915ff597 Mon Sep 17 00:00:00 2001
From: Anton Kovsharov <antonkovsharov@gmail.com>
Date: Thu, 25 Jan 2024 14:14:40 +0000
Subject: [PATCH] Move parser to use InfoTree.visitM instead of manual
 traversal to adapt for https://github.com/leanprover/lean4/pull/3159

---
 lean/BetterParser.lean | 11 ++++-------
 lean/Paperproof.lean   | 19 +++++++++++--------
 2 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/lean/BetterParser.lean b/lean/BetterParser.lean
index 68c1930..544fb0a 100644
--- a/lean/BetterParser.lean
+++ b/lean/BetterParser.lean
@@ -152,12 +152,10 @@ def nameNumLt (n1 n2 : Name) : Bool :=
   | .num _ _,  _ => true
   | _, _ => false
 
-partial def BetterParser (context: Option ContextInfo) (infoTree : InfoTree) : RequestM Result :=
-  match context, infoTree with
-  | some (ctx : ContextInfo), .node i cs => do
+partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree) (res : List (Option Result)) : RequestM Result := do
+    let res := res.filterMap id
     let some ctx := i.updateContext? ctx
       | panic! "unexpected context node"
-    let res ← cs.toList.mapM (BetterParser ctx)
     let steps := res.map (fun r => r.steps) |>.join
     let allSubGoals := HashSet.empty.insertMany $ res.bind (·.allGoals.toList)
     if let .ofTacticInfo tInfo := i then
@@ -194,6 +192,5 @@ partial def BetterParser (context: Option ContextInfo) (infoTree : InfoTree) : R
       return { steps := newSteps ++ steps, allGoals }
     else
       return { steps, allGoals := allSubGoals}
-  | none, .node .. => panic! "unexpected context-free info tree node"
-  | _, .context ctx t => BetterParser ctx t
-  | _, .hole .. => pure {steps := [], allGoals := .empty}
+
+partial def BetterParser (i : InfoTree) := i.visitM (postNode := postNode)
diff --git a/lean/Paperproof.lean b/lean/Paperproof.lean
index d4898ca..2f957f6 100644
--- a/lean/Paperproof.lean
+++ b/lean/Paperproof.lean
@@ -18,11 +18,14 @@ def getSnapshotData (params : InputParams) : RequestM (RequestTask OutputParams)
   withWaitFindSnapAtPos params.pos fun snap => do
     checkIfUserIsStillTyping snap params.pos
 
-    let parsedTree ← BetterParser none snap.infoTree
-    -- This happens when we hover over something other than a theorem
-    if (parsedTree.steps.length == 0) then
-      throwThe RequestError ⟨.invalidParams, "zeroProofSteps"⟩
-    return {
-      steps := parsedTree.steps,
-      version := 2
-    }
+    let parsedTree? ← BetterParser snap.infoTree
+    match parsedTree? with
+    | none => throwThe RequestError ⟨.invalidParams, "noParsedTree"⟩
+    | some parsedTree => do
+      -- This happens when we hover over something other than a theorem
+      if (parsedTree.steps.length == 0) then
+        throwThe RequestError ⟨.invalidParams, "zeroProofSteps"⟩
+      return {
+        steps := parsedTree.steps,
+        version := 2
+      }