fix: new page between ToC and pre-chapter content (#715)

Author: david-christiansen

src/tests/integration/code-content-doc/expected/tex/main.tex

@@ -121,6 +121,7 @@
 \tableofcontents
 
 
+\cleardoublepage
 Here is some code with vertical bars:
 \begin{LeanVerbatim}
 \textbf{def} or := (· \symbol{124}\symbol{124} ·)

src/tests/integration/front-matter-doc/expected/tex/main.tex

@@ -121,6 +121,7 @@
 \tableofcontents
 
 
+\cleardoublepage
 This is the introduction text that appears before any chapters.
 It should be part of the front matter.
 \chapter{Preface}

src/tests/integration/inheritance-doc/expected/tex/main.tex

@@ -121,6 +121,7 @@
 \tableofcontents
 
 
+\cleardoublepage
 \begin{docstringBox}{structure}
 \LeanVerb|Verso.Integration.InheritanceDoc.FooExtends : Type|\tcblower Documentation for FooExtends\par\noindent\textbf{Constructor}\par \par \LeanVerb|Verso.Integration.InheritanceDoc.FooExtends.mk|\par\noindent\textbf{Extends}\par Verso.Integration.InheritanceDoc.FooExtends\par\noindent\textbf{Fields}\par \par \LeanVerb|barField1| : \LeanVerb|Bool|\par Inherited from \LeanVerb|BarExtended|\par \LeanVerb|barField2| : \LeanVerb|Unit|\par Inherited from \LeanVerb|BarExtended|\par \LeanVerb|fooField1| : \LeanVerb|Nat|\par Documentation for fooField1\par \LeanVerb|fooField2| : \LeanVerb|String|\par Documentation for fooField2
 \end{docstringBox}

src/tests/integration/sample-doc/expected/tex/main.tex

@@ -121,6 +121,7 @@
 \tableofcontents
 
 
+\cleardoublepage
 \begin{docstringBox}{def}
 \LeanVerb|Verso.Integration.SampleDoc.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|

src/verso-manual/VersoManual.lean

@@ -373,7 +373,11 @@ def emitTeX (logError : String → IO Unit) (config : Config) (text : Part Manua
     if config.verbose then
       IO.println s!"Saving {dir.join "main.tex"}"
     h.putStrLn (preamble text.titleString authors date packages.toList preambleItems.toList)
-    -- \frontmatter is inserted by our hardcoded preamble
+    -- \frontmatter is inserted by our hardcoded preamble before the ToC, so it doesn't get inserted
+    -- here. If there's any text at the start of the front matter, then we need to clear it to a new
+    -- recto page after the ToC
+    unless frontText.all (·.isEmpty) do
+      h.putStrLn "\\cleardoublepage"
     for b in frontMatter do
       h.putStrLn b.asString
     h.putStrLn "\n\\mainmatter"

src/verso/Verso/Doc.lean

@@ -167,6 +167,11 @@ public def Inline.other (container : genre.Inline) (content : Array (Inline genr
 
 public def Inline.empty : Inline genre := .concat #[]
 
+public def Inline.isEmpty : Inline genre → Bool
+  | .text s => s.isEmpty
+  | .concat xs => xs.attach.all fun ⟨x, _⟩ => x.isEmpty
+  | .code .. | .linebreak .. | .image .. | .link .. | .math .. | .other .. | .footnote .. | .bold .. | .emph .. => false
+
 public partial def Inline.rewriteOtherM [Monad m]
     (onInline :
       (Inline genre1 → m (Inline genre2)) →
@@ -446,6 +451,20 @@ public instance : Append (Lean.Doc.Block i b) where
 
 public def Block.empty : Block genre := .concat #[]
 
+public def Block.isEmpty : Block genre → Bool
+  | .concat xs | .blockquote xs => xs.attach.all fun ⟨x, _⟩ => x.isEmpty
+  | .para xs => xs.all (·.isEmpty)
+  | .code .. | .other ..=> false
+  | .ol _ xs | .ul xs => xs.attach.all fun ⟨⟨x⟩, _⟩ => x.attach.all fun ⟨y, _⟩ =>
+    y.isEmpty
+  | .dl xs => xs.attach.all fun ⟨⟨x, y⟩, _⟩ =>
+    (x.attach.all fun ⟨x', _⟩ => x'.isEmpty) && (y.attach.all fun ⟨y', _⟩ => y'.isEmpty)
+decreasing_by
+  all_goals (try decreasing_tactic)
+  all_goals
+    have := Array.sizeOf_lt_of_mem ‹_ ∈ xs›
+    grind
+
 public partial def Block.rewriteOtherM [Monad m]
     (onInline :
       (Inline genre1 → m (Inline genre2)) →