src/Pure/Thy/latex.ML
author wenzelm
Thu Mar 19 15:44:14 2009 +0100 (2009-03-19)
changeset 30589 cbe27c4ef417
parent 30573 49899f26fbd1
child 30590 1d9c9fcf8513
permissions -rw-r--r--
Antiquote.Text: keep full position information;
     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: OuterLex.token -> 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 
    34 (* symbol output *)
    35 
    36 local
    37 
    38 val output_chr = fn
    39   " " => "\\ " |
    40   "\n" => "\\isanewline\n" |
    41   "!" => "{\\isacharbang}" |
    42   "\"" => "{\\isachardoublequote}" |
    43   "#" => "{\\isacharhash}" |
    44   "$" => "{\\isachardollar}" |
    45   "%" => "{\\isacharpercent}" |
    46   "&" => "{\\isacharampersand}" |
    47   "'" => "{\\isacharprime}" |
    48   "(" => "{\\isacharparenleft}" |
    49   ")" => "{\\isacharparenright}" |
    50   "*" => "{\\isacharasterisk}" |
    51   "+" => "{\\isacharplus}" |
    52   "," => "{\\isacharcomma}" |
    53   "-" => "{\\isacharminus}" |
    54   "." => "{\\isachardot}" |
    55   "/" => "{\\isacharslash}" |
    56   ":" => "{\\isacharcolon}" |
    57   ";" => "{\\isacharsemicolon}" |
    58   "<" => "{\\isacharless}" |
    59   "=" => "{\\isacharequal}" |
    60   ">" => "{\\isachargreater}" |
    61   "?" => "{\\isacharquery}" |
    62   "@" => "{\\isacharat}" |
    63   "[" => "{\\isacharbrackleft}" |
    64   "\\" => "{\\isacharbackslash}" |
    65   "]" => "{\\isacharbrackright}" |
    66   "^" => "{\\isacharcircum}" |
    67   "_" => "{\\isacharunderscore}" |
    68   "`" => "{\\isacharbackquote}" |
    69   "{" => "{\\isacharbraceleft}" |
    70   "|" => "{\\isacharbar}" |
    71   "}" => "{\\isacharbraceright}" |
    72   "~" => "{\\isachartilde}" |
    73   c => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c;
    74 
    75 val output_chrs = translate_string output_chr;
    76 
    77 fun output_known_sym (known_sym, known_ctrl) sym =
    78   (case Symbol.decode sym of
    79     Symbol.Char s => output_chr s
    80   | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
    81   | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
    82   | Symbol.Raw s => s);
    83 
    84 in
    85 
    86 val output_known_symbols = implode oo (map o output_known_sym);
    87 val output_symbols = output_known_symbols (K true, K true);
    88 val output_syms = output_symbols o Symbol.explode;
    89 
    90 val output_syms_antiq =
    91   (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
    92     | Antiquote.Antiq (ss, _) =>
    93         enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
    94     | Antiquote.Open _ => "{\\isaantiqopen}"
    95     | Antiquote.Close _ => "{\\isaantiqclose}");
    96 
    97 end;
    98 
    99 
   100 (* token output *)
   101 
   102 structure T = OuterLex;
   103 
   104 val invisible_token = T.keyword_with (fn s => s = ";") orf T.is_kind T.Comment;
   105 
   106 fun output_basic tok =
   107   let val s = T.content_of tok in
   108     if invisible_token tok then ""
   109     else if T.is_kind T.Command tok then
   110       "\\isacommand{" ^ output_syms s ^ "}"
   111     else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
   112       "\\isakeyword{" ^ output_syms s ^ "}"
   113     else if T.is_kind T.String tok then
   114       enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
   115     else if T.is_kind T.AltString tok then
   116       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   117     else if T.is_kind T.Verbatim tok then
   118       let
   119         val (txt, pos) = T.source_position_of tok;
   120         val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
   121         val out = implode (map output_syms_antiq ants);
   122       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   123     else output_syms s
   124   end;
   125 
   126 fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n";
   127 
   128 fun output_markup_env cmd txt =
   129   "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
   130   Symbol.strip_blanks txt ^
   131   "%\n\\end{isamarkup" ^ cmd ^ "}%\n";
   132 
   133 fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
   134 
   135 val markup_true = "\\isamarkuptrue%\n";
   136 val markup_false = "\\isamarkupfalse%\n";
   137 
   138 val begin_delim = enclose "%\n\\isadelim" "\n";
   139 val end_delim = enclose "%\n\\endisadelim" "\n";
   140 val begin_tag = enclose "%\n\\isatag" "\n";
   141 fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
   142 
   143 
   144 (* theory presentation *)
   145 
   146 val tex_trailer =
   147   "%%% Local Variables:\n\
   148   \%%% mode: latex\n\
   149   \%%% TeX-master: \"root\"\n\
   150   \%%% End:\n";
   151 
   152 fun isabelle_file name txt =
   153   "%\n\\begin{isabellebody}%\n\
   154   \\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
   155   "\\end{isabellebody}%\n" ^ tex_trailer;
   156 
   157 fun symbol_source known name syms = isabelle_file name
   158   ("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
   159     output_known_symbols known syms);
   160 
   161 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
   162 
   163 
   164 (* print mode *)
   165 
   166 val latexN = "latex";
   167 val modes = [latexN, Symbol.xsymbolsN];
   168 
   169 fun latex_output str =
   170   let val syms = Symbol.explode str
   171   in (output_symbols syms, Symbol.length syms) end;
   172 
   173 fun latex_markup (s, _) =
   174   if s = Markup.keywordN then ("\\isakeyword{", "}")
   175   else if s = Markup.commandN then ("\\isacommand{", "}")
   176   else Markup.no_output;
   177 
   178 fun latex_indent "" _ = ""
   179   | latex_indent s _ = enclose "\\isaindent{" "}" s;
   180 
   181 val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
   182 val _ = Markup.add_mode latexN latex_markup;
   183 val _ = Pretty.add_mode latexN latex_indent;
   184 
   185 end;