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