src/Pure/Thy/latex.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23703 1b6a2c119151
child 27344 d44490b06190
permissions -rw-r--r--
Name.uu, Name.aT;
     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_antiqs =
    92   Antiquote.scan_antiquotes #> map
    93   (fn Antiquote.Text s => output_syms s
    94     | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)) #>
    95   implode;
    96 
    97 end;
    98 
    99 
   100 (* token output *)
   101 
   102 structure T = OuterLex;
   103 
   104 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
   105 
   106 fun output_basic tok =
   107   let val s = T.val_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       enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
   119         (output_syms_antiqs (s, T.position_of tok))
   120     else output_syms s
   121   end;
   122 
   123 fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n";
   124 
   125 fun output_markup_env cmd txt =
   126   "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
   127   Symbol.strip_blanks txt ^
   128   "%\n\\end{isamarkup" ^ cmd ^ "}%\n";
   129 
   130 fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
   131 
   132 val markup_true = "\\isamarkuptrue%\n";
   133 val markup_false = "\\isamarkupfalse%\n";
   134 
   135 val begin_delim = enclose "%\n\\isadelim" "\n";
   136 val end_delim = enclose "%\n\\endisadelim" "\n";
   137 val begin_tag = enclose "%\n\\isatag" "\n";
   138 fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
   139 
   140 
   141 (* theory presentation *)
   142 
   143 val tex_trailer =
   144   "%%% Local Variables:\n\
   145   \%%% mode: latex\n\
   146   \%%% TeX-master: \"root\"\n\
   147   \%%% End:\n";
   148 
   149 fun isabelle_file name txt =
   150   "%\n\\begin{isabellebody}%\n\
   151   \\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
   152   "\\end{isabellebody}%\n" ^ tex_trailer;
   153 
   154 fun symbol_source known name syms = isabelle_file name
   155   ("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
   156     output_known_symbols known syms);
   157 
   158 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
   159 
   160 
   161 (* print mode *)
   162 
   163 val latexN = "latex";
   164 val modes = [latexN, Symbol.xsymbolsN];
   165 
   166 fun latex_output str =
   167   let val syms = Symbol.explode str
   168   in (output_symbols syms, Symbol.length syms) end;
   169 
   170 fun latex_markup (s, _) =
   171   if s = Markup.keywordN then ("\\isakeyword{", "}")
   172   else if s = Markup.commandN then ("\\isacommand{", "}")
   173   else ("", "");
   174 
   175 fun latex_indent "" _ = ""
   176   | latex_indent s _ = enclose "\\isaindent{" "}" s;
   177 
   178 val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
   179 val _ = Markup.add_mode latexN latex_markup;
   180 val _ = Pretty.add_mode latexN latex_indent;
   181 
   182 end;