fix: do not include leading file contents in blog genre lean blocks as whitespace (#924)

leanprover/lean4#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.

Fixes #923.

Author: whxvd

src/verso-blog/VersoBlog.lean

@@ -488,7 +488,7 @@ meta 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