Skip to content

fix: preserve paragraphs in docstring boxes in TeX output (#918) #919

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
david-christiansen merged 4 commits into from
Jul 30, 2026
Merged

fix: preserve paragraphs in docstring boxes in TeX output (#918) #919

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f9cd7eb
fix: preserve paragraphs in docstring boxes in TeX output (#918)
medovina Jul 9, 2026
bc62358
Merge branch 'main' into docstringbox-paragraphs
medovina Jul 28, 2026
ab1997f
chore: fix integration tests
medovina Jul 28, 2026
3cbc3ac
chore: revert several files committed by mistake
medovina Jul 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/tests/integration/code-content-doc/expected/tex/main.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@
\definecolor{bordercolor}{HTML}{98B2C0}
\definecolor{medgray}{HTML}{555555}
\newtcolorbox{docstringBox}[2][]{colback=white,
before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box
breakable,
colframe=bordercolor,
colbacktitle=white,
Expand Down
1 change: 1 addition & 0 deletions src/tests/integration/diagram-doc/expected/tex/main.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@
\definecolor{bordercolor}{HTML}{98B2C0}
\definecolor{medgray}{HTML}{555555}
\newtcolorbox{docstringBox}[2][]{colback=white,
before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box
breakable,
colframe=bordercolor,
colbacktitle=white,
Expand Down
1 change: 1 addition & 0 deletions src/tests/integration/escape-doc/expected/tex/main.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@
\definecolor{bordercolor}{HTML}{98B2C0}
\definecolor{medgray}{HTML}{555555}
\newtcolorbox{docstringBox}[2][]{colback=white,
before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box
breakable,
colframe=bordercolor,
colbacktitle=white,
Expand Down
1 change: 1 addition & 0 deletions src/tests/integration/extra-files-doc/expected/tex/main.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@
\definecolor{bordercolor}{HTML}{98B2C0}
\definecolor{medgray}{HTML}{555555}
\newtcolorbox{docstringBox}[2][]{colback=white,
before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box
breakable,
colframe=bordercolor,
colbacktitle=white,
Expand Down
1 change: 1 addition & 0 deletions src/tests/integration/front-matter-doc/expected/tex/main.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@
\definecolor{bordercolor}{HTML}{98B2C0}
\definecolor{medgray}{HTML}{555555}
\newtcolorbox{docstringBox}[2][]{colback=white,
before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box
breakable,
colframe=bordercolor,
colbacktitle=white,
Expand Down
11 changes: 10 additions & 1 deletion src/tests/integration/inheritance-doc/expected/tex/main.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@
\definecolor{bordercolor}{HTML}{98B2C0}
\definecolor{medgray}{HTML}{555555}
\newtcolorbox{docstringBox}[2][]{colback=white,
before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box
breakable,
colframe=bordercolor,
colbacktitle=white,
Expand Down Expand Up @@ -143,7 +144,15 @@

\cleardoublepage
\begin{docstringBox}{structure}
\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends : Type|\tcblower Documentation for FooExtends\par\noindent\textbf{Constructor}\par \par \LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends.\allowbreak{}mk|\par\noindent\textbf{Extends}\par Verso.Integration.InheritanceDoc.FooExtends\par\noindent\textbf{Fields}\par \par \LeanVerb|bar\-Field1| : \LeanVerb|Bool|\par Inherited from \LeanVerb|Bar\-Extended|\par \LeanVerb|bar\-Field2| : \LeanVerb|Unit|\par Inherited from \LeanVerb|Bar\-Extended|\par \LeanVerb|foo\-Field1| : \LeanVerb|Nat|\par Documentation for fooField1\par \LeanVerb|foo\-Field2| : \LeanVerb|String|\par Documentation for fooField2
\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends : Type|\tcblower Documentation for FooExtends

\par\noindent\textbf{Constructor}\par \par\noindent \LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends.\allowbreak{}mk|

\par\noindent\textbf{Extends}\par Verso.Integration.InheritanceDoc.FooExtends

\par\noindent\textbf{Fields}\par \par\noindent \LeanVerb|bar\-Field1| : \LeanVerb|Bool|\par Inherited from \LeanVerb|Bar\-Extended|\par\noindent \LeanVerb|bar\-Field2| : \LeanVerb|Unit|\par Inherited from \LeanVerb|Bar\-Extended|\par\noindent \LeanVerb|foo\-Field1| : \LeanVerb|Nat|\par Documentation for fooField1\par\noindent \LeanVerb|foo\-Field2| : \LeanVerb|String|\par Documentation for fooField2


\end{docstringBox}


Expand Down
11 changes: 9 additions & 2 deletions src/tests/integration/sample-doc/expected/tex/main.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@
\definecolor{bordercolor}{HTML}{98B2C0}
\definecolor{medgray}{HTML}{555555}
\newtcolorbox{docstringBox}[2][]{colback=white,
before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box
breakable,
colframe=bordercolor,
colbacktitle=white,
Expand Down Expand Up @@ -143,9 +144,15 @@

\cleardoublepage
\begin{docstringBox}{def}
\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Sample\-Doc.\allowbreak{}sample_constant : Type|\tcblower This is a docstring.Here's some more text with a \LeanVerb|code inline| in it.
\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Sample\-Doc.\allowbreak{}sample_constant : Type|\tcblower This is a docstring.

Here's some more text with a \LeanVerb|code inline| in it.
Here's when a \LeanVerb|code inline|
occurs right before a line break.And then here's a paragraph break.
occurs right before a line break.

And then here's a paragraph break.


\end{docstringBox}

Here is a test of \LeanVerb|escaping of things like \symbol{92}TeX in code inlines|
Expand Down
7 changes: 4 additions & 3 deletions src/verso-manual/VersoManual/Docstring.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -613,7 +613,7 @@ def internalSignature.descr : BlockDescr where
if let some sig := signature then
pure \TeX{ " : " \Lean{ (← sig.toTeX) } }
else pure .empty
pure \TeX{\par " " \Lean{← name.toTeX} \Lean{signatureTeX} \Lean{.seq (← contents.mapM goB)}}
pure \TeX{\par\noindent " " \Lean{← name.toTeX} \Lean{signatureTeX} \Lean{.seq (← contents.mapM goB)}}
toHtml := some fun _goI goB _id info contents =>
open Verso.Doc.Html HtmlT in
open Verso.Output Html in do
Expand Down Expand Up @@ -675,7 +675,7 @@ def fieldSignature.descr : BlockDescr where
| .public => .empty
| .private => \TeX{ \textbf{"private"} }
| .protected => .empty
let desc := \TeX{ \par " " \Lean{visibility} \Lean{← name.toTeX} " : " \Lean{← signature.toTeX} \par " " \Lean{.seq (← contents.mapM goB)}}
let desc := \TeX{ \par\noindent " " \Lean{visibility} \Lean{← name.toTeX} " : " \Lean{← signature.toTeX} \par " " \Lean{.seq (← contents.mapM goB)}}
let parentsTeX := (← parents.toList.mapM (·.toTeX)).intersperse (.raw ", ")
let inheritedExtra : Output.TeX := match inheritedFrom with
| .none => ""
Expand Down Expand Up @@ -889,7 +889,8 @@ def docstring.descr : BlockDescr := withHighlighting {
let label := customLabel.getD declType.label
if label == "" then
reportError s!"Missing label for '{name}': supply one with 'label := \"LABEL\"'"
pure \TeX{\begin{docstringBox}{\Lean{label}} \Lean{← signature.toTeX} \tcblower " " \Lean{← contents.mapM goB} \end{docstringBox}}
pure \TeX{\begin{docstringBox}{\Lean{label}} \Lean{← signature.toTeX} \tcblower " "
\Lean{← contents.mapM (fun b => do pure <| seq #[← goB b, .paragraphBreak])} \end{docstringBox}}

extraCss := [docstringStyle]
}
Expand Down
1 change: 1 addition & 0 deletions src/verso-manual/VersoManual/TeX.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,7 @@ r##"
\definecolor{bordercolor}{HTML}{98B2C0}
\definecolor{medgray}{HTML}{555555}
\newtcolorbox{docstringBox}[2][]{colback=white,
before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box
breakable,
colframe=bordercolor,
colbacktitle=white,
Expand Down