src/Pure/Thy/latex.ML

--- a/src/Pure/Thy/latex.ML	Fri May 21 13:07:53 2021 +0200
+++ b/src/Pure/Thy/latex.ML	Sat May 22 13:35:25 2021 +0200
@@ -34,6 +34,7 @@
   val index_item: index_item -> text
   type index_entry = {items: index_item list, def: bool}
   val index_entry: index_entry -> text
+  val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
   val latexN: string
   val latex_output: string -> string * int
   val latex_markup: string * Properties.T -> Markup.output
@@ -258,7 +259,8 @@
 
 val index_escape =
   translate_string (fn s =>
-    s |> exists_string (fn s' => s = s') "\"\\{}!@|" ? prefix "\"");
+    if member_string "!\"@|" s then "\\char" ^ string_of_int (ord s)
+    else if member_string "\\{}#" s then "\"" ^ s else s);
 
 fun index_item (item: index_item) =
   let
@@ -273,6 +275,13 @@
   |> enclose_block "\\index{" "}";
 
 
+fun index_binding NONE = I
+  | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
+
+fun index_variants setup binding =
+  fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
+
+
 (* print mode *)
 
 val latexN = "latex";