From 96d1928647cc24817433511bb318bf78438d00cf Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Tue, 30 Apr 2024 09:41:48 +0200
Subject: [PATCH] fix: deep tactic state dedup

---
 .../SubVerso/Highlighting/Code.lean           | 23 +++++++++++++++----
 .../SubVerso/Highlighting/Highlighted.lean    |  4 ++++
 2 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean
index 4d7922a..327df59 100644
--- a/src/highlighting/SubVerso/Highlighting/Code.lean
+++ b/src/highlighting/SubVerso/Highlighting/Code.lean
@@ -314,14 +314,27 @@ where
 
 abbrev HighlightM (α : Type) : Type := StateT HighlightState TermElabM α
 
-def HighlightState.openTactic (st : HighlightState) (info : Array (Highlighted.Goal Highlighted)) (bytePos : Nat) (pos : Position) : HighlightState := Id.run do
-  if let .tactics info' pos' :: output' := st.output then
-    if bytePos == pos' then
-      return {st with output := .tactics (info ++ info') pos' :: output'}
-  return {st with
+private def modify? (f : α → Option α) : (xs : List α) → Option (List α)
+  | [] => none
+  | x :: xs =>
+    if let some x' := f x then
+      some (x' :: xs)
+    else (x :: ·) <$> modify? f xs
+
+def HighlightState.openTactic (st : HighlightState) (info : Array (Highlighted.Goal Highlighted)) (bytePos : Nat) (pos : Position) : HighlightState :=
+  if let some out' := modify? update? st.output then
+    {st with output := out'}
+  else {st with
     output := .tactics info bytePos :: st.output,
     inMessages := .inr ⟨pos⟩ :: st.inMessages
   }
+where
+  update?
+    | .tactics info' pos' =>
+      if bytePos == pos' then
+        some <| .tactics (info ++ info') pos'
+      else none
+    | _ => none
 
 def HighlightM.openTactic (info : Array (Highlighted.Goal Highlighted)) (bytePos : Nat) (pos : Position) : HighlightM Unit :=
   modify fun st => st.openTactic info bytePos pos
diff --git a/src/highlighting/SubVerso/Highlighting/Highlighted.lean b/src/highlighting/SubVerso/Highlighting/Highlighted.lean
index d4e3910..5bc8a25 100644
--- a/src/highlighting/SubVerso/Highlighting/Highlighted.lean
+++ b/src/highlighting/SubVerso/Highlighting/Highlighted.lean
@@ -76,6 +76,10 @@ inductive Highlighted where
   | seq (highlights : Array Highlighted)
   -- TODO replace messages as strings with structured info
   | span (info : Array (Highlighted.Span.Kind × String)) (content : Highlighted)
+  /--
+  A saved tactic state. The `pos` parameter indicates the byte index in the file where this tactic
+  state ceases; this is used for deduplication and rendering and gives a unique ID.
+  -/
   | tactics (info : Array (Highlighted.Goal Highlighted)) (pos : Nat) (content : Highlighted)
   | point (kind : Highlighted.Span.Kind) (info : String)
 deriving Repr, Inhabited, BEq, Hashable, ToJson, FromJson