fix: trailing whitespace for syntax that contains trailing nulls (#696)

Author: david-christiansen

src/tests/Tests/CommentSkipping.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
 import Tests.CommentSkipping.Doc
+import Tests.CommentSkipping.Doc2
 
 /-!
 This test ensures that Lean's parser doesn't skip Lean comment syntax while parsing Verso blocks as
@@ -27,3 +28,17 @@ info: Verso.Doc.Part.mk
 -/
 #guard_msgs in
 #eval %doc Tests.CommentSkipping.Doc
+
+/--
+info: Verso.Doc.Part.mk
+  #[Verso.Doc.Inline.text "Title"]
+  "Title"
+  none
+  #[Verso.Doc.Block.blockquote #[],
+    Verso.Doc.Block.blockquote
+      #[(Verso.Doc.Block.para #[Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "abc")] "http://example.com"])],
+    Verso.Doc.Block.blockquote #[(Verso.Doc.Block.para #[Verso.Doc.Inline.text "C", Verso.Doc.Inline.linebreak "\n"])]]
+  #[]
+-/
+#guard_msgs in
+#eval %doc Tests.CommentSkipping.Doc2

src/tests/Tests/CommentSkipping/Doc2.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import Verso
+
+/-!
+This test checks a regression that happened where syntax that contained trailing null nodes wouldn't
+have trailing whitespace updated properly, leading to failed parses.
+-/
+
+
+
+#doc (.none) "Title" =>
+
+
+>
+> [abc](http://example.com)
+
+> C

src/verso/Verso/Doc/Concrete.lean

@@ -139,14 +139,31 @@ private meta partial def updateSyntaxTrailing (trailing : Substring.Raw) : Synta
   | .atom info val => .atom (updateInfoTrailing trailing info) val
   | .ident info rawVal val pre => .ident (updateInfoTrailing trailing info) rawVal val pre
   | n@(.node info k args) =>
-    if h : args.size = 0 then n
-    else
-     let i    := args.size - 1
+    if let some i := findIdxRev? (not ∘ empty) args then
      let last := updateSyntaxTrailing trailing args[i]
      let args := args.set i last;
      Syntax.node info k args
+    else n
   | s => s
 where
+  findIdxRev? {α} (p : α → Bool) (xs : Array α) : Option (Fin xs.size) := do
+    if h : xs.size = 0 then failure
+    else
+      let mut n : Fin xs.size := ⟨xs.size - 1, by grind⟩
+      repeat
+        if p xs[n] then return n
+        if n.val = 0 then
+          break
+        else
+          n := ⟨n.val - 1, by grind⟩
+      failure
+
+  empty : Syntax → Bool
+  | .atom .. | .ident .. | .missing => false
+  | .node .none _ args | .node (.synthetic ..) _ args => args.all empty
+  | .node (.original leading _ trailing _) _ args =>
+    leading.startPos == leading.stopPos && trailing.startPos == trailing.stopPos && args.all empty
+
   updateInfoTrailing (trailing : Substring.Raw) : SourceInfo → SourceInfo
     | .original leading pos _ endPos => .original leading pos trailing endPos
     | .none =>
@@ -199,8 +216,9 @@ where
     let top := s.stxStack.back
     if let some ⟨_, tr⟩ := getTailContext? c.fileMap.source top then
       let tr := { tr with stopPos := s.pos }
-      s.popSyntax.pushSyntax (updateSyntaxTrailing tr top)
-    else s
+      s.popSyntax.pushSyntax <| updateSyntaxTrailing tr top
+    else
+      s
 
 /--
 As we elaborate a `#doc` command top-level-block by top-level-block, the Lean environment will