src/Pure/Thy/latex.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59123 e68e44836d04
child 59809 87641097d0f3
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     1 (*  Title:      Pure/Thy/latex.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 LaTeX presentation elements -- based on outer lexical syntax.
     5 *)
     6 
     7 signature LATEX =
     8 sig
     9   val output_ascii: string -> string
    10   val output_known_symbols: (string -> bool) * (string -> bool) ->
    11     Symbol.symbol list -> string
    12   val output_symbols: Symbol.symbol list -> string
    13   val output_basic: Token.T -> string
    14   val output_markup: string -> string -> string
    15   val output_markup_env: string -> string -> string
    16   val output_verbatim: string -> string
    17   val markup_true: string
    18   val markup_false: string
    19   val begin_delim: string -> string
    20   val end_delim: string -> string
    21   val begin_tag: string -> string
    22   val end_tag: string -> string
    23   val tex_trailer: string
    24   val isabelle_theory: string -> string -> string
    25   val symbol_source: (string -> bool) * (string -> bool) ->
    26     string -> Symbol.symbol list -> string
    27   val theory_entry: string -> string
    28   val modes: string list
    29 end;
    30 
    31 structure Latex: LATEX =
    32 struct
    33 
    34 (* literal ASCII *)
    35 
    36 val output_ascii =
    37   translate_string
    38     (fn " " => "\\ "
    39       | "\t" => "\\ "
    40       | "\n" => "\\isanewline\n"
    41       | s =>
    42           if exists_string (fn s' => s = s') "#$%^&_{}~\\<>"
    43           then enclose "{\\char`\\" "}" s else s);
    44 
    45 
    46 (* symbol output *)
    47 
    48 local
    49 
    50 val char_table =
    51   Symtab.make
    52    [("!", "{\\isacharbang}"),
    53     ("\"", "{\\isachardoublequote}"),
    54     ("#", "{\\isacharhash}"),
    55     ("$", "{\\isachardollar}"),
    56     ("%", "{\\isacharpercent}"),
    57     ("&", "{\\isacharampersand}"),
    58     ("'", "{\\isacharprime}"),
    59     ("(", "{\\isacharparenleft}"),
    60     (")", "{\\isacharparenright}"),
    61     ("*", "{\\isacharasterisk}"),
    62     ("+", "{\\isacharplus}"),
    63     (",", "{\\isacharcomma}"),
    64     ("-", "{\\isacharminus}"),
    65     (".", "{\\isachardot}"),
    66     ("/", "{\\isacharslash}"),
    67     (":", "{\\isacharcolon}"),
    68     (";", "{\\isacharsemicolon}"),
    69     ("<", "{\\isacharless}"),
    70     ("=", "{\\isacharequal}"),
    71     (">", "{\\isachargreater}"),
    72     ("?", "{\\isacharquery}"),
    73     ("@", "{\\isacharat}"),
    74     ("[", "{\\isacharbrackleft}"),
    75     ("\\", "{\\isacharbackslash}"),
    76     ("]", "{\\isacharbrackright}"),
    77     ("^", "{\\isacharcircum}"),
    78     ("_", "{\\isacharunderscore}"),
    79     ("`", "{\\isacharbackquote}"),
    80     ("{", "{\\isacharbraceleft}"),
    81     ("|", "{\\isacharbar}"),
    82     ("}", "{\\isacharbraceright}"),
    83     ("~", "{\\isachartilde}")];
    84 
    85 fun output_chr " " = "\\ "
    86   | output_chr "\t" = "\\ "
    87   | output_chr "\n" = "\\isanewline\n"
    88   | output_chr c =
    89       (case Symtab.lookup char_table c of
    90         SOME s => s
    91       | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
    92 
    93 val output_chrs = translate_string output_chr;
    94 
    95 fun output_known_sym (known_sym, known_ctrl) sym =
    96   (case Symbol.decode sym of
    97     Symbol.Char s => output_chr s
    98   | Symbol.UTF8 s => s
    99   | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
   100   | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
   101   | Symbol.Raw s => s
   102   | Symbol.Malformed s => error (Symbol.malformed_msg s)
   103   | Symbol.EOF => error "Bad EOF symbol");
   104 
   105 in
   106 
   107 val output_known_symbols = implode oo (map o output_known_sym);
   108 val output_symbols = output_known_symbols (K true, K true);
   109 val output_syms = output_symbols o Symbol.explode;
   110 
   111 val output_syms_antiq =
   112   (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
   113     | Antiquote.Antiq (ss, _) =>
   114         enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
   115           (output_symbols (map Symbol_Pos.symbol ss)));
   116 
   117 end;
   118 
   119 
   120 (* token output *)
   121 
   122 fun output_basic tok =
   123   let val s = Token.content_of tok in
   124     if Token.is_kind Token.Comment tok then ""
   125     else if Token.is_command tok then
   126       "\\isacommand{" ^ output_syms s ^ "}"
   127     else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
   128       "\\isakeyword{" ^ output_syms s ^ "}"
   129     else if Token.is_kind Token.String tok then
   130       enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
   131     else if Token.is_kind Token.Alt_String tok then
   132       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   133     else if Token.is_kind Token.Verbatim tok then
   134       let
   135         val ants = Antiquote.read (Token.source_position_of tok);
   136         val out = implode (map output_syms_antiq ants);
   137       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   138     else if Token.is_kind Token.Cartouche tok then
   139       enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
   140     else output_syms s
   141   end;
   142 
   143 fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n";
   144 
   145 fun output_markup_env cmd txt =
   146   "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
   147   Symbol.strip_blanks txt ^
   148   "%\n\\end{isamarkup" ^ cmd ^ "}%\n";
   149 
   150 fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
   151 
   152 val markup_true = "\\isamarkuptrue%\n";
   153 val markup_false = "\\isamarkupfalse%\n";
   154 
   155 val begin_delim = enclose "%\n\\isadelim" "\n";
   156 val end_delim = enclose "%\n\\endisadelim" "\n";
   157 val begin_tag = enclose "%\n\\isatag" "\n";
   158 fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
   159 
   160 
   161 (* theory presentation *)
   162 
   163 val tex_trailer =
   164   "%%% Local Variables:\n\
   165   \%%% mode: latex\n\
   166   \%%% TeX-master: \"root\"\n\
   167   \%%% End:\n";
   168 
   169 fun isabelle_theory name txt =
   170   "%\n\\begin{isabellebody}%\n\
   171   \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
   172   "\\end{isabellebody}%\n" ^ tex_trailer;
   173 
   174 fun symbol_source known name syms =
   175   isabelle_theory name
   176     ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
   177       output_known_symbols known syms);
   178 
   179 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
   180 
   181 
   182 (* print mode *)
   183 
   184 val latexN = "latex";
   185 val modes = [latexN, Symbol.xsymbolsN];
   186 
   187 fun latex_output str =
   188   let val syms = Symbol.explode str
   189   in (output_symbols syms, Symbol.length syms) end;
   190 
   191 fun latex_markup (s, _) =
   192   if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
   193   then ("\\isacommand{", "}")
   194   else if s = Markup.keyword2N
   195   then ("\\isakeyword{", "}")
   196   else Markup.no_output;
   197 
   198 fun latex_indent "" _ = ""
   199   | latex_indent s _ = enclose "\\isaindent{" "}" s;
   200 
   201 val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
   202 val _ = Markup.add_mode latexN latex_markup;
   203 val _ = Pretty.add_mode latexN latex_indent;
   204 
   205 end;