From 28e18d39774079c9434439b35d967cb352ef41c8 Mon Sep 17 00:00:00 2001
From: Jessica Clarke
Date: Wed, 7 Oct 2020 00:29:43 +0100
Subject: latex: Guard abbreviations with \@

Otherwise they will be typeset as if the end of a sentence, causing
additional spacing after the '.' when not using \frenchspacing.
---
 src/latex.ml | 14 +++++++++++++-
 src/sail.ml  |  8 ++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/latex.ml b/src/latex.ml
index 9cb0b4d8..14c8cdca 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -59,6 +59,7 @@ module StringSet = Set.Make(String);;
 let opt_prefix = ref "sail"
 let opt_directory = ref "sail_latex"
 let opt_simple_val = ref true
+let opt_abbrevs = ref ["e.g."; "i.e."]
 
 let rec unique_postfix n =
   if n < 0 then
@@ -220,8 +221,18 @@ let refcode_string = refcode_cat_string Val
 
 let inline_code str = sprintf "\\lstinline{%s}" str
 
+let guard_abbrevs str =
+  let frags = List.map Str.quote !opt_abbrevs in
+  let alternation = String.concat "\\|" frags in
+  let regex = Str.regexp ("\\b\\(" ^ alternation ^ "\\)\\( \\|$\\)") in
+  (* We use this seemingly-unnecessary wrapper so consumers like
+     cheri-architecture that want to use \xpatch on our output don't run into
+     issues like https://tex.stackexchange.com/q/565659/175942. *)
+  Str.global_replace regex "\\saildocabbrev{\\1}\\2" str
+
 let text_code str =
   str
+  |> guard_abbrevs
   |> Str.global_replace (Str.regexp_string "_") "\\_"
   |> Str.global_replace (Str.regexp_string ">") "$<$"
   |> Str.global_replace (Str.regexp_string "<") "$>$"
@@ -446,7 +457,8 @@ let defs { defs; _ } =
     "\\providecommand\\saildocfcl[2]{#1 #2}\n" ^
     "\\providecommand\\saildoctype[2]{#1 #2}\n" ^
     "\\providecommand\\saildocfn[2]{#1 #2}\n" ^
-    "\\providecommand\\saildocoverload[2]{#1 #2}\n\n") in
+    "\\providecommand\\saildocoverload[2]{#1 #2}\n" ^
+    "\\providecommand\\saildocabbrev[1]{#1\\@}\n\n") in
 
   let overload_counter = ref 0 in
 
diff --git a/src/sail.ml b/src/sail.ml
index 38d4c2e8..5a1ad096 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -166,6 +166,14 @@ let options = Arg.align ([
   ( "-latex_full_valspecs",
     Arg.Clear Latex.opt_simple_val,
     " print full valspecs in LaTeX output");
+  ( "-latex_abbrevs",
+    Arg.String (fun s ->
+      let abbrevs = String.split_on_char ';' s in
+      let filtered = List.filter (fun abbrev -> not (String.equal "" abbrev)) abbrevs in
+      match List.find_opt (fun abbrev -> not (String.equal "." (String.sub abbrev (String.length abbrev - 1) 1))) filtered with
+      | None -> Latex.opt_abbrevs := filtered
+      | Some abbrev -> raise (Arg.Bad (abbrev ^ " does not end in a '.'"))),
+    " semicolon-separated list of abbreviations to fix spacing for in LaTeX output (default 'e.g.;i.e.')");
   ( "-marshal",
     Arg.Tuple [set_target "marshal"; Arg.Set Initial_check.opt_undefined_gen],
     " OCaml-marshal out the rewritten AST to a file");
-- 
cgit v1.2.3