diff --git a/src/tests/integration/code-content-doc/expected/tex/main.tex b/src/tests/integration/code-content-doc/expected/tex/main.tex index 4d245fe9d..dc5c4add1 100644 --- a/src/tests/integration/code-content-doc/expected/tex/main.tex +++ b/src/tests/integration/code-content-doc/expected/tex/main.tex @@ -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, diff --git a/src/tests/integration/diagram-doc/expected/tex/main.tex b/src/tests/integration/diagram-doc/expected/tex/main.tex index 47d521914..cae367de9 100644 --- a/src/tests/integration/diagram-doc/expected/tex/main.tex +++ b/src/tests/integration/diagram-doc/expected/tex/main.tex @@ -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, diff --git a/src/tests/integration/escape-doc/expected/tex/main.tex b/src/tests/integration/escape-doc/expected/tex/main.tex index 643e68e0e..ad10c55ff 100644 --- a/src/tests/integration/escape-doc/expected/tex/main.tex +++ b/src/tests/integration/escape-doc/expected/tex/main.tex @@ -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, diff --git a/src/tests/integration/extra-files-doc/expected/tex/main.tex b/src/tests/integration/extra-files-doc/expected/tex/main.tex index c9aa89ea8..0e510661d 100644 --- a/src/tests/integration/extra-files-doc/expected/tex/main.tex +++ b/src/tests/integration/extra-files-doc/expected/tex/main.tex @@ -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, diff --git a/src/tests/integration/front-matter-doc/expected/tex/main.tex b/src/tests/integration/front-matter-doc/expected/tex/main.tex index 371a84f8e..7da5a0b40 100644 --- a/src/tests/integration/front-matter-doc/expected/tex/main.tex +++ b/src/tests/integration/front-matter-doc/expected/tex/main.tex @@ -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, diff --git a/src/tests/integration/inheritance-doc/expected/tex/main.tex b/src/tests/integration/inheritance-doc/expected/tex/main.tex index 0600aab1b..1a8eba05f 100644 --- a/src/tests/integration/inheritance-doc/expected/tex/main.tex +++ b/src/tests/integration/inheritance-doc/expected/tex/main.tex @@ -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, @@ -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} diff --git a/src/tests/integration/sample-doc/expected/tex/main.tex b/src/tests/integration/sample-doc/expected/tex/main.tex index 7d0f48a24..5dcb18dd7 100644 --- a/src/tests/integration/sample-doc/expected/tex/main.tex +++ b/src/tests/integration/sample-doc/expected/tex/main.tex @@ -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, @@ -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| diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 3fc84fb51..1a5e9bba0 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -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 @@ -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 => "" @@ -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] } diff --git a/src/verso-manual/VersoManual/TeX.lean b/src/verso-manual/VersoManual/TeX.lean index 96ff529b9..1fb30e9ab 100644 --- a/src/verso-manual/VersoManual/TeX.lean +++ b/src/verso-manual/VersoManual/TeX.lean @@ -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,