src/Pure/Thy/latex.ML
changeset 67145 e77c5bfca9aa
parent 66021 08ab52fb9db5
child 67173 e746db6db903
     1.1 --- a/src/Pure/Thy/latex.ML	Wed Dec 06 09:11:27 2017 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed Dec 06 14:19:36 2017 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature LATEX =
     1.6  sig
     1.7 +  val output_name: string -> string
     1.8    val output_ascii: string -> string
     1.9    val latex_control: Symbol.symbol
    1.10    val is_latex_control: Symbol.symbol -> bool
    1.11 @@ -13,6 +14,7 @@
    1.12    val output_known_symbols: (string -> bool) * (string -> bool) ->
    1.13      Symbol.symbol list -> string
    1.14    val output_symbols: Symbol.symbol list -> string
    1.15 +  val output_syms: string -> string
    1.16    val output_token: Token.T -> string
    1.17    val begin_delim: string -> string
    1.18    val end_delim: string -> string
    1.19 @@ -30,6 +32,27 @@
    1.20  structure Latex: LATEX =
    1.21  struct
    1.22  
    1.23 +(* output name for LaTeX macros *)
    1.24 +
    1.25 +val output_name =
    1.26 +  translate_string
    1.27 +    (fn "_" => "UNDERSCORE"
    1.28 +      | "'" => "PRIME"
    1.29 +      | "0" => "ZERO"
    1.30 +      | "1" => "ONE"
    1.31 +      | "2" => "TWO"
    1.32 +      | "3" => "THREE"
    1.33 +      | "4" => "FOUR"
    1.34 +      | "5" => "FIVE"
    1.35 +      | "6" => "SIX"
    1.36 +      | "7" => "SEVEN"
    1.37 +      | "8" => "EIGHT"
    1.38 +      | "9" => "NINE"
    1.39 +      | s => s);
    1.40 +
    1.41 +fun enclose_name bg en = enclose bg en o output_name;
    1.42 +
    1.43 +
    1.44  (* output verbatim ASCII *)
    1.45  
    1.46  val output_ascii =
    1.47 @@ -101,8 +124,8 @@
    1.48    (case Symbol.decode sym of
    1.49      Symbol.Char s => output_chr s
    1.50    | Symbol.UTF8 s => s
    1.51 -  | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
    1.52 -  | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
    1.53 +  | Symbol.Sym s => if known_sym s then enclose_name "{\\isasym" "}" s else output_chrs sym
    1.54 +  | Symbol.Control s => if known_ctrl s then enclose_name "\\isactrl" " " s else output_chrs sym
    1.55    | Symbol.Malformed s => error (Symbol.malformed_msg s)
    1.56    | Symbol.EOF => error "Bad EOF symbol");
    1.57  
    1.58 @@ -173,16 +196,16 @@
    1.59  
    1.60  (* tags *)
    1.61  
    1.62 -val begin_delim = enclose "%\n\\isadelim" "\n";
    1.63 -val end_delim = enclose "%\n\\endisadelim" "\n";
    1.64 -val begin_tag = enclose "%\n\\isatag" "\n";
    1.65 -fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
    1.66 +val begin_delim = enclose_name "%\n\\isadelim" "\n";
    1.67 +val end_delim = enclose_name "%\n\\endisadelim" "\n";
    1.68 +val begin_tag = enclose_name "%\n\\isatag" "\n";
    1.69 +fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
    1.70  
    1.71  
    1.72  (* theory presentation *)
    1.73  
    1.74  fun environment name =
    1.75 -  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}");
    1.76 +  enclose ("%\n\\begin{" ^ output_name name ^ "}%\n") ("%\n\\end{" ^ output_name name ^ "}");
    1.77  
    1.78  val tex_trailer =
    1.79    "%%% Local Variables:\n\