name mangling for Latex macros;
authorwenzelm
Wed Dec 06 14:19:36 2017 +0100 (6 weeks ago)
changeset 67145e77c5bfca9aa
parent 67142 fa1173288322
child 67146 909dcdec2122
name mangling for Latex macros;
tuned signature;
NEWS
src/Pure/Thy/latex.ML
     1.1 --- a/NEWS	Wed Dec 06 09:11:27 2017 +0100
     1.2 +++ b/NEWS	Wed Dec 06 14:19:36 2017 +0100
     1.3 @@ -78,6 +78,11 @@
     1.4  tagged as "document" and visible by default. This avoids the application
     1.5  of option "document_tags" to these commands.
     1.6  
     1.7 +* Isabelle names are mangled into LaTeX macro names to allow the full
     1.8 +identifier syntax with underscore, prime, digits. This is relevant for
     1.9 +antiquotations in control symbol notation, e.g. \<^const_name> becomes
    1.10 +\isactrlconstUNDERSCOREname.
    1.11 +
    1.12  
    1.13  *** HOL ***
    1.14  
     2.1 --- a/src/Pure/Thy/latex.ML	Wed Dec 06 09:11:27 2017 +0100
     2.2 +++ b/src/Pure/Thy/latex.ML	Wed Dec 06 14:19:36 2017 +0100
     2.3 @@ -6,6 +6,7 @@
     2.4  
     2.5  signature LATEX =
     2.6  sig
     2.7 +  val output_name: string -> string
     2.8    val output_ascii: string -> string
     2.9    val latex_control: Symbol.symbol
    2.10    val is_latex_control: Symbol.symbol -> bool
    2.11 @@ -13,6 +14,7 @@
    2.12    val output_known_symbols: (string -> bool) * (string -> bool) ->
    2.13      Symbol.symbol list -> string
    2.14    val output_symbols: Symbol.symbol list -> string
    2.15 +  val output_syms: string -> string
    2.16    val output_token: Token.T -> string
    2.17    val begin_delim: string -> string
    2.18    val end_delim: string -> string
    2.19 @@ -30,6 +32,27 @@
    2.20  structure Latex: LATEX =
    2.21  struct
    2.22  
    2.23 +(* output name for LaTeX macros *)
    2.24 +
    2.25 +val output_name =
    2.26 +  translate_string
    2.27 +    (fn "_" => "UNDERSCORE"
    2.28 +      | "'" => "PRIME"
    2.29 +      | "0" => "ZERO"
    2.30 +      | "1" => "ONE"
    2.31 +      | "2" => "TWO"
    2.32 +      | "3" => "THREE"
    2.33 +      | "4" => "FOUR"
    2.34 +      | "5" => "FIVE"
    2.35 +      | "6" => "SIX"
    2.36 +      | "7" => "SEVEN"
    2.37 +      | "8" => "EIGHT"
    2.38 +      | "9" => "NINE"
    2.39 +      | s => s);
    2.40 +
    2.41 +fun enclose_name bg en = enclose bg en o output_name;
    2.42 +
    2.43 +
    2.44  (* output verbatim ASCII *)
    2.45  
    2.46  val output_ascii =
    2.47 @@ -101,8 +124,8 @@
    2.48    (case Symbol.decode sym of
    2.49      Symbol.Char s => output_chr s
    2.50    | Symbol.UTF8 s => s
    2.51 -  | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
    2.52 -  | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
    2.53 +  | Symbol.Sym s => if known_sym s then enclose_name "{\\isasym" "}" s else output_chrs sym
    2.54 +  | Symbol.Control s => if known_ctrl s then enclose_name "\\isactrl" " " s else output_chrs sym
    2.55    | Symbol.Malformed s => error (Symbol.malformed_msg s)
    2.56    | Symbol.EOF => error "Bad EOF symbol");
    2.57  
    2.58 @@ -173,16 +196,16 @@
    2.59  
    2.60  (* tags *)
    2.61  
    2.62 -val begin_delim = enclose "%\n\\isadelim" "\n";
    2.63 -val end_delim = enclose "%\n\\endisadelim" "\n";
    2.64 -val begin_tag = enclose "%\n\\isatag" "\n";
    2.65 -fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
    2.66 +val begin_delim = enclose_name "%\n\\isadelim" "\n";
    2.67 +val end_delim = enclose_name "%\n\\endisadelim" "\n";
    2.68 +val begin_tag = enclose_name "%\n\\isatag" "\n";
    2.69 +fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
    2.70  
    2.71  
    2.72  (* theory presentation *)
    2.73  
    2.74  fun environment name =
    2.75 -  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}");
    2.76 +  enclose ("%\n\\begin{" ^ output_name name ^ "}%\n") ("%\n\\end{" ^ output_name name ^ "}");
    2.77  
    2.78  val tex_trailer =
    2.79    "%%% Local Variables:\n\