From 392171ddf9b782d1c06eacecacc2fa74ca815b0d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 30 Apr 2024 09:03:06 +0200 Subject: [PATCH] fix: de-nest tactics for the same location --- src/highlighting/SubVerso/Highlighting/Code.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean index 1181f35..802dc08 100644 --- a/src/highlighting/SubVerso/Highlighting/Code.lean +++ b/src/highlighting/SubVerso/Highlighting/Code.lean @@ -208,8 +208,11 @@ def Output.addText (output : List Output) (str : String) : List Output := def Output.openSpan (output : List Output) (messages : Array (Highlighted.Span.Kind × String)) : List Output := .span messages :: output -def Output.openTactic (output : List Output) (info : Array (Highlighted.Goal Highlighted)) (pos : Nat) : List Output := - .tactics info pos :: output +def Output.openTactic (output : List Output) (info : Array (Highlighted.Goal Highlighted)) (pos : Nat) : List Output := Id.run do + if let .tactics info' pos' :: output' := output then + if pos == pos' then + return .tactics (info ++ info') pos :: output' + return .tactics info pos :: output def Output.inTacticState (output : List Output) (info : Array (Highlighted.Goal Highlighted)) : Bool := output.any fun