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