From 5068e62c19265c775740469a9f994147b2445de7 Mon Sep 17 00:00:00 2001 From: Sebastian Miele Date: Mon, 13 Jul 2026 11:58:34 +0200 Subject: [PATCH] fix: do not include leading file contents in blog genre `lean` blocks as whitespace https://github.com/leanprover/lean4/pull/12662 changed the module parser to by default include the text preceding the first token in a Lean file as whitespace belonging to that token. That parser infrastructure also is used for `lean` blocks in the blog genre. The change in the PR had the effect that the first `lean` block for an `exampleContext` always included the whole preceding Verso file contents as leading whitespace at the first command token. See https://leanprover.zulipchat.com/#narrow/channel/576452-verso/topic/Text.20rendering.20twice/with/608642094 for screenshots. --- src/verso-blog/VersoBlog.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index 83fbfb7ce..4e01fc7b2 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -480,7 +480,7 @@ def lean : CodeBlockExpanderOf LeanBlockConfig -- Process with empty messages to avoid duplicate output let s ← withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Elaborating commands") <| - IO.processCommands context { state with pos := startPos } { commandState with messages.unreported := {} } + IO.processCommands context { state with pos := startPos, hasLeading := false } { commandState with messages.unreported := {} } for t in s.commandState.infoState.trees do pushInfoTree t