From 953b60c89461071b454404776bc3b4c2e00997b4 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 19 Feb 2026 16:13:12 +0100 Subject: [PATCH] fix: rendering of hygiene info nodes in Verso docstring code blocks (#12594) This PR fixes a bug with rendering of hygiene info nodes in embedded Verso code examples. The embedded anonymous identifier was being rendered as [anonymous] instead of being omitted. --- src/Lean/Elab/DocString/Builtin.lean | 7 ++ tests/lean/run/versoDocs.lean | 122 +++++++++++++++++++++++++++ 2 files changed, 129 insertions(+) diff --git a/src/Lean/Elab/DocString/Builtin.lean b/src/Lean/Elab/DocString/Builtin.lean index 7017710d88..093dbaa447 100644 --- a/src/Lean/Elab/DocString/Builtin.lean +++ b/src/Lean/Elab/DocString/Builtin.lean @@ -786,6 +786,13 @@ where match stx with | .node info kind args => emitLeading info + if kind == hygieneInfoKind then + -- hygieneInfo nodes contain no source text; skip content but preserve whitespace + for arg in args do + emitLeading arg.getHeadInfo + emitTrailing arg.getHeadInfo + emitTrailing info + return if isLitKind kind then match args with | #[.atom info' str] => diff --git a/tests/lean/run/versoDocs.lean b/tests/lean/run/versoDocs.lean index 73c38f91bb..2bd1edd015 100644 --- a/tests/lean/run/versoDocs.lean +++ b/tests/lean/run/versoDocs.lean @@ -632,3 +632,125 @@ Self-module references should work without `-checked`. -/ /-! {module}`lean.run.versoDocs` -/ + +/-! +Test that {lit}`hygieneInfo` nodes in syntax (produced by parenthesized expressions) don't introduce +spurious {lit}`[anonymous]` strings into highlighted code blocks and inline roles. +-/ + +section HygieneInfoTests +open Doc Elab + +private def ppDoc (code : Array (String × Option DocHighlight)) : Std.Format := + .group (behavior := .fill) <| code.foldl (init := .nil) fun + | soFar, (str, none) => soFar.append str + | soFar, (str, some hl) => soFar ++ .line ++ (entaggen hl str) +where + entaggen hl str := (opener hl : Format) ++ str ++ closer hl + opener + | .const x sig => s!"" + | .var x fv ty => s!"" + | .field x sig => s!"" + | .option x d => s!"" + | .var .. => "" + | .field .. => "" + | .option .. => "" + | .keyword => "" + | .literal .. => "" + +private def docCodeStr (dc : DocCode) : String := + ppDoc dc.code |>.pretty (width := 70) + +private partial def findInInline (name : Name) : Inline ElabInline → Array DocCode + | .other container _ => + if container.name == name then + if let some (lt : Data.LeanTerm) := container.val.get? Data.LeanTerm then + #[lt.term] + else #[] + else #[] + | .emph xs | .bold xs | .concat xs | .link xs _ | .footnote _ xs => + xs.flatMap (findInInline name) + | .text .. | .code .. | .math .. | .linebreak .. | .image .. => #[] + +private partial def findInBlock (name : Name) : Block ElabInline ElabBlock → Array DocCode + | .other container _ => + if container.name == name then + if let some (lb : Data.LeanBlock) := container.val.get? Data.LeanBlock then + #[lb.commands] + else if let some (lt : Data.LeanTerm) := container.val.get? Data.LeanTerm then + #[lt.term] + else #[] + else #[] + | .para inlines => inlines.flatMap (findInInline name) + | .concat blocks | .blockquote blocks => blocks.flatMap (findInBlock name) + | .dl items => items.flatMap fun ⟨x, y⟩ => x.flatMap (findInInline name) ++ y.flatMap (findInBlock name) + | .ol _ xs | .ul xs => xs.flatMap fun ⟨x⟩ => x.flatMap (findInBlock name) + | .code .. => #[] + +-- Lean code block: tests `highlightSyntax` for command sequences +/-- +```lean +#eval (2 * (5 + 1) + (5 + 1)) +``` +-/ +def testHygieneCodeBlock := () + +/-- +info: #eval ( 2 ⏎ +* ( 5 + ⏎ +1 ) + ( +5 + ⏎ +1 ) ) + +-/ +#guard_msgs in +#eval show TermElabM Unit from do + let some (.inr doc) ← findInternalDocString? (← getEnv) ``testHygieneCodeBlock + | throwError "expected verso doc" + doc.text.flatMap (findInBlock ``Data.LeanBlock) |>.map docCodeStr |>.forM (IO.println ·) + +-- Inline `lean` role: tests `highlightSyntax` for inline terms +/-- +The value is {lean}`(2 * (5 + 1) + (5 + 1))`. +-/ +def testHygieneInlineRole := () + +/-- +info: ( 2 * ( +5 + ⏎ +1 ) + ( +5 + ⏎ +1 ) ) +-/ +#guard_msgs in +#eval show TermElabM Unit from do + let some (.inr doc) ← findInternalDocString? (← getEnv) ``testHygieneInlineRole + | throwError "expected verso doc" + doc.text.flatMap (findInBlock ``Data.LeanTerm) |>.map docCodeStr |>.forM (IO.println ·) + +-- `leanTerm` code block: tests `highlightSyntax` for block-level terms +/-- +```leanTerm +(2 * (5 + 1))...34 +``` +-/ +def testHygieneTermBlock := () + +/-- +info: ( 2 * ( +5 + ⏎ +1 ) ) ... +34 +-/ +#guard_msgs in +#eval show TermElabM Unit from do + let some (.inr doc) ← findInternalDocString? (← getEnv) ``testHygieneTermBlock + | throwError "expected verso doc" + doc.text.flatMap (findInBlock ``Data.LeanTerm) |>.map docCodeStr |>.forM (IO.println ·) + +end HygieneInfoTests