Skip to content

fix: preserve paragraphs in recommended spelling descriptions - #399

Merged
hargoniX merged 1 commit into
leanprover:mainfrom
skwh54:fix/recommended-spelling-line-breaks
Aug 3, 2026
Merged

hargoniX merged 1 commit into
leanprover:mainfrom
skwh54:fix/recommended-spelling-line-breaks

Conversation

@skwh54

@skwh54 skwh54 commented Jul 28, 2026

Copy link
Copy Markdown
Contributor

Fixes #398.

Summary

Preserve spaces and paragraph boundaries when rendering multiline recommended_spelling descriptions as Verso content.

Consecutive non-empty source lines are joined with spaces, while blank lines produce separate paragraphs. Existing behavior for absent and single-line descriptions remains unchanged.

Root cause

The additional information was split into lines and combined using String.join, which inserts no separator. This concatenated adjacent words and discarded paragraph boundaries.

Lean's string representation preserves line breaks and blank lines when generating Markdown. This change mirrors the resulting soft-wrap and paragraph structure using Verso blocks.

Verification

Rendered the reproduction from the linked issue using both the baseline and patched versions of doc-gen4. The Lean input was identical in both builds.

Before

<p>First paragraph spansmultiple source lines.Second paragraph.</p>
image

After

<p>First paragraph spans multiple source lines.</p>
<p>Second paragraph.</p>
image

Both documentation builds completed successfully with Lean v4.33.0-rc1, and the generated pages were served locally over HTTP and verified in Chromium.

@hargoniX
hargoniX merged commit b08f503 into leanprover:main Aug 3, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Multiline recommended_spelling descriptions lose spaces and paragraph boundaries

2 participants