# HG changeset patch
# User wenzelm
# Date 1512566376 -3600
# Node ID e77c5bfca9aae297469bb6e815d72da6bf5eb42d
# Parent  fa1173288322a146f659d513bf5e752fc25a6d6a
name mangling for Latex macros;
tuned signature;

diff -r fa1173288322 -r e77c5bfca9aa NEWS
--- a/NEWS	Wed Dec 06 09:11:27 2017 +0100
+++ b/NEWS	Wed Dec 06 14:19:36 2017 +0100
@@ -78,6 +78,11 @@
 tagged as "document" and visible by default. This avoids the application
 of option "document_tags" to these commands.
 
+* Isabelle names are mangled into LaTeX macro names to allow the full
+identifier syntax with underscore, prime, digits. This is relevant for
+antiquotations in control symbol notation, e.g. \<^const_name> becomes
+\isactrlconstUNDERSCOREname.
+
 
 *** HOL ***
 
diff -r fa1173288322 -r e77c5bfca9aa src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Dec 06 09:11:27 2017 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Dec 06 14:19:36 2017 +0100
@@ -6,6 +6,7 @@
 
 signature LATEX =
 sig
+  val output_name: string -> string
   val output_ascii: string -> string
   val latex_control: Symbol.symbol
   val is_latex_control: Symbol.symbol -> bool
@@ -13,6 +14,7 @@
   val output_known_symbols: (string -> bool) * (string -> bool) ->
     Symbol.symbol list -> string
   val output_symbols: Symbol.symbol list -> string
+  val output_syms: string -> string
   val output_token: Token.T -> string
   val begin_delim: string -> string
   val end_delim: string -> string
@@ -30,6 +32,27 @@
 structure Latex: LATEX =
 struct
 
+(* output name for LaTeX macros *)
+
+val output_name =
+  translate_string
+    (fn "_" => "UNDERSCORE"
+      | "'" => "PRIME"
+      | "0" => "ZERO"
+      | "1" => "ONE"
+      | "2" => "TWO"
+      | "3" => "THREE"
+      | "4" => "FOUR"
+      | "5" => "FIVE"
+      | "6" => "SIX"
+      | "7" => "SEVEN"
+      | "8" => "EIGHT"
+      | "9" => "NINE"
+      | s => s);
+
+fun enclose_name bg en = enclose bg en o output_name;
+
+
 (* output verbatim ASCII *)
 
 val output_ascii =
@@ -101,8 +124,8 @@
   (case Symbol.decode sym of
     Symbol.Char s => output_chr s
   | Symbol.UTF8 s => s
-  | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
-  | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
+  | Symbol.Sym s => if known_sym s then enclose_name "{\\isasym" "}" s else output_chrs sym
+  | Symbol.Control s => if known_ctrl s then enclose_name "\\isactrl" " " s else output_chrs sym
   | Symbol.Malformed s => error (Symbol.malformed_msg s)
   | Symbol.EOF => error "Bad EOF symbol");
 
@@ -173,16 +196,16 @@
 
 (* tags *)
 
-val begin_delim = enclose "%\n\\isadelim" "\n";
-val end_delim = enclose "%\n\\endisadelim" "\n";
-val begin_tag = enclose "%\n\\isatag" "\n";
-fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
+val begin_delim = enclose_name "%\n\\isadelim" "\n";
+val end_delim = enclose_name "%\n\\endisadelim" "\n";
+val begin_tag = enclose_name "%\n\\isatag" "\n";
+fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
 
 
 (* theory presentation *)
 
 fun environment name =
-  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}");
+  enclose ("%\n\\begin{" ^ output_name name ^ "}%\n") ("%\n\\end{" ^ output_name name ^ "}");
 
 val tex_trailer =
   "%%% Local Variables:\n\