feat: soft breaking in PDF identifiers (#720)

Adds soft-breaking rules for identifiers in PDF mode, so the hboxes can
be less overfull.

Author: david-christiansen

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

@@ -143,7 +143,7 @@
 
 \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
+\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
 \end{docstringBox}
 
 

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

@@ -143,7 +143,7 @@
 
 \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.
+\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.
 \end{docstringBox}

src/verso/Verso/Code/HighlightedToTex.lean

@@ -39,42 +39,45 @@ public def highlightToken : String → Token.Kind → TeX
 | c, .withType _ => .raw c
 | c, .unknown => .raw c
 
-defmethod Highlighting.Token.toVerbatimTeX (t : Highlighting.Token) : Verso.Output.TeX :=
-  highlightToken (escapeForVerbatim t.content) t.kind
+defmethod Highlighting.Token.toVerbatimTeX (t : Highlighting.Token) (lineBreaks : Bool := false) : Verso.Output.TeX :=
+  highlightToken (escapeForVerbatim t.content lineBreaks) t.kind
 
 open Verso.Output.TeX in
 /--
 Returns TeX that is appropriate for the content of a `\Verb` environment (from package `fancyvrb`)
 with command characters `\`, `{`, and `}`.
+
+When `lineBreaks` is true, inserts line break opportunities in identifiers.
 -/
-public defmethod Highlighted.toVerbatimTeX : Highlighted → Verso.Output.TeX
-  | .token t => highlightToken (escapeForVerbatim t.content) t.kind
-  | .text str => .raw (escapeForVerbatim str)
-  | .seq hts => .seq <| hts.map (·.toVerbatimTeX)
+public defmethod Highlighted.toVerbatimTeX (h : Highlighted) (lineBreaks : Bool := false) : Verso.Output.TeX :=
+  match h with
+  | .token t => highlightToken (escapeForVerbatim t.content lineBreaks) t.kind
+  | .text str => .raw (escapeForVerbatim str lineBreaks)
+  | .seq hts => .seq <| hts.map (·.toVerbatimTeX lineBreaks)
   | .span info content =>
      if h : info.size > 0
-     then .seq #[.raw s!"\\{info[0].1.toString}Decorate\{", content.toVerbatimTeX, .raw "}"]
-     else content.toVerbatimTeX
-  | .tactics _info _start _end content => content.toVerbatimTeX
+     then .seq #[.raw s!"\\{info[0].1.toString}Decorate\{", content.toVerbatimTeX lineBreaks, .raw "}"]
+     else content.toVerbatimTeX lineBreaks
+  | .tactics _info _start _end content => content.toVerbatimTeX lineBreaks
   | .point _kind _info => \TeX{"[Point]"}
-  | .unparsed str => .raw (escapeForVerbatim str)
+  | .unparsed str => .raw (escapeForVerbatim str lineBreaks)
 
 def verbatimBlock (t : Verso.Output.TeX) : Verso.Output.TeX :=
   .seq #[.raw "\\begin{LeanVerbatim}\n", t, .raw "\n\\end{LeanVerbatim}\n"]
 
 public defmethod Highlighting.Token.toTeX [Monad m] [GenreTeX g m] (t : Highlighting.Token) :
     TeXT g m Verso.Output.TeX :=
-  verbatimInline (t.toVerbatimTeX)
+  verbatimInline (t.toVerbatimTeX (lineBreaks := true))
 
 public defmethod Highlighted.toTeX [Monad m] [GenreTeX g m] (t : Highlighted) :
     TeXT g m Verso.Output.TeX :=
   let strip := t.trimOneTrailingNl.trimOneLeadingNl
   if strip.isEmpty then
     pure .empty
   else if strip.containsNewline then
-    pure <| verbatimBlock (strip.toVerbatimTeX)
+    pure <| verbatimBlock (strip.toVerbatimTeX (lineBreaks := false))
   else
-    verbatimInline (strip.toVerbatimTeX)
+    verbatimInline (strip.toVerbatimTeX (lineBreaks := true))
 
 
 open Verso.Output.TeX in

src/verso/Verso/Doc/TeX.lean

@@ -105,23 +105,103 @@ def replaceChars (s : String) (replace : Char → Option String) : String :=
   loop "" 0
 
 /--
-Escapes a string in an appropriate way for uses of `\Verb` and
+Escapes a single character in an appropriate way for uses of `\Verb` and
 `\begin{Verbatim}...\end{Verbatim}` (from package `fancyvrb`) with
 command characters `\`, `{`, and `}`.
 -/
-public def escapeForVerbatim (s : String) : String :=
-  replaceChars s fun
+private def escapeCharForVerbatim (c : Char) : Option String :=
+  match c with
   | '{' => some "\\symbol{123}"
   | '|' => some "\\symbol{124}"
   | '}' => some "\\symbol{125}"
   | '\\' => some "\\symbol{92}"
   | '#' => some "\\symbol{35}" -- FIXME: this is really just a test
   | _ => none
 
+/--
+Tracks the previous character class for inserting line break opportunities.
+-/
+private inductive PrevChar
+  /-- previous was lowercase letter -/
+  | lower
+  /-- previous was digit -/
+  | digit
+  /-- previous was '.' -/
+  | dot
+  /-- initial / anything else -/
+  | other
+
+/--
+Escapes a string in an appropriate way for uses of `\Verb` and
+`\begin{Verbatim}...\end{Verbatim}` (from package `fancyvrb`) with
+command characters `\`, `{`, and `}`.
+
+When `lineBreaks` is true, inserts line break opportunities:
+- After `.`: insert `\allowbreak{}` (no hyphen on break)
+- On lowercase→uppercase transition: insert `\-` (soft hyphen)
+- On digit→letter transition: insert `\-` (soft hyphen)
+-/
+public def escapeForVerbatim (s : String) (lineBreaks : Bool := false) : String :=
+  if !lineBreaks then
+    replaceChars s escapeCharForVerbatim
+  else Id.run do
+    let mut state : PrevChar := .other
+    let mut result : String := ""
+    for c in s.toList do
+      -- Emit break if transition warrants it
+      let break_ := match state with
+        | .dot => if c != '.' then "\\allowbreak{}" else ""
+        | .lower => if c.isUpper then "\\-" else ""
+        | .digit => if c.isAlpha then "\\-" else ""
+        | .other => ""
+      -- Emit escaped char
+      let escaped := escapeCharForVerbatim c |>.getD c.toString
+      -- Update state
+      state :=
+        if c.isLower then .lower
+        else if c.isDigit then .digit
+        else if c == '.' then .dot
+        else .other
+      result := result ++ break_ ++ escaped
+    return result
+
 /-- info: "\\symbol{123}\\symbol{124}\\symbol{125}\\symbol{92}" -/
 #guard_msgs in
 #eval escapeForVerbatim "{|}\\"
 
+-- Tests for lineBreaks functionality
+/-- info: "Nat.\\allowbreak{}add\\-One" -/
+#guard_msgs in
+#eval escapeForVerbatim "Nat.addOne" (lineBreaks := true)
+
+/-- info: "List.\\allowbreak{}map2\\-Fun" -/
+#guard_msgs in
+#eval escapeForVerbatim "List.map2Fun" (lineBreaks := true)
+
+/-- info: "x2\\-y" -/
+#guard_msgs in
+#eval escapeForVerbatim "x2y" (lineBreaks := true)
+
+/-- info: "Foo123" -/
+#guard_msgs in
+#eval escapeForVerbatim "Foo123" (lineBreaks := true)  -- no break before digits
+
+/-- info: "a..\\allowbreak{}b" -/
+#guard_msgs in
+#eval escapeForVerbatim "a..b" (lineBreaks := true)  -- only one break after dot sequence
+
+/-- info: "\\symbol{123}foo\\-Bar" -/
+#guard_msgs in
+#eval escapeForVerbatim "{fooBar" (lineBreaks := true)  -- escaping + line breaks
+
+/-- info: "plain" -/
+#guard_msgs in
+#eval escapeForVerbatim "plain" (lineBreaks := true)  -- no transitions
+
+/-- info: "Nat.addOne" -/
+#guard_msgs in
+#eval escapeForVerbatim "Nat.addOne"  -- lineBreaks := false (default), no breaks
+
 /--
 Wraps some TeX (which is already assumed to be appropriately escaped in the appropriate
 verbatim-like environment depending on whether we're in a fragile environment.