src/Pure/Thy/latex.ML
author wenzelm
Sat Aug 09 22:43:46 2008 +0200 (2008-08-09)
changeset 27809 a1e409db516b
parent 27781 5a82ee34e9fc
child 27874 f0364f1c0ecf
permissions -rw-r--r--
unified Args.T with OuterLex.token, renamed some operations;
     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 val output_syms' = output_symbols o map #1 o SymbolPos.explode;
    91 
    92 val output_syms_antiqs =
    93   Antiquote.read #> map
    94   (fn Antiquote.Text s => output_syms s
    95     | Antiquote.Antiq x => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms' x)
    96     | Antiquote.Open _ => "{\\isaantiqopen}"
    97     | Antiquote.Close _ => "{\\isaantiqclose}") #>
    98   implode;
    99 
   100 end;
   101 
   102 
   103 (* token output *)
   104 
   105 structure T = OuterLex;
   106 
   107 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
   108 
   109 fun output_basic tok =
   110   let val s = T.content_of tok in
   111     if invisible_token tok then ""
   112     else if T.is_kind T.Command tok then
   113       "\\isacommand{" ^ output_syms s ^ "}"
   114     else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
   115       "\\isakeyword{" ^ output_syms s ^ "}"
   116     else if T.is_kind T.String tok then
   117       enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
   118     else if T.is_kind T.AltString tok then
   119       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   120     else if T.is_kind T.Verbatim tok then
   121       enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
   122         (output_syms_antiqs (s, T.position_of tok))
   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 ("", "");
   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;