wenzelm@7726: (*  Title:      Pure/Thy/latex.ML
wenzelm@7726:     ID:         $Id$
wenzelm@7726:     Author:     Markus Wenzel, TU Muenchen
wenzelm@7726: 
wenzelm@15801: LaTeX presentation elements -- based on outer lexical syntax.
wenzelm@7726: *)
wenzelm@7726: 
wenzelm@7726: signature LATEX =
wenzelm@7726: sig
wenzelm@14924:   val output_known_symbols: (string -> bool) * (string -> bool) ->
wenzelm@14924:     Symbol.symbol list -> string
berghofe@11719:   val output_symbols: Symbol.symbol list -> string
wenzelm@17081:   val output_basic: OuterLex.token -> string
wenzelm@17081:   val output_markup: string -> string -> string
wenzelm@17081:   val output_markup_env: string -> string -> string
wenzelm@17081:   val output_verbatim: string -> string
wenzelm@17081:   val markup_true: string
wenzelm@17081:   val markup_false: string
wenzelm@17081:   val begin_delim: string -> string
wenzelm@17081:   val end_delim: string -> string
wenzelm@17081:   val begin_tag: string -> string
wenzelm@17081:   val end_tag: string -> string
wenzelm@9707:   val tex_trailer: string
wenzelm@9916:   val isabelle_file: string -> string -> string
wenzelm@14924:   val symbol_source: (string -> bool) * (string -> bool) ->
wenzelm@14924:     string -> Symbol.symbol list -> string
wenzelm@7726:   val theory_entry: string -> string
wenzelm@9135:   val modes: string list
wenzelm@7726: end;
wenzelm@7726: 
wenzelm@7726: structure Latex: LATEX =
wenzelm@7726: struct
wenzelm@7726: 
wenzelm@7726: 
wenzelm@7726: (* symbol output *)
wenzelm@7726: 
wenzelm@7900: local
wenzelm@7900: 
wenzelm@7726: val output_chr = fn
wenzelm@9505:   " " => "\\ " |
wenzelm@7726:   "\n" => "\\isanewline\n" |
wenzelm@9668:   "!" => "{\\isacharbang}" |
wenzelm@9668:   "\"" => "{\\isachardoublequote}" |
wenzelm@9663:   "#" => "{\\isacharhash}" |
wenzelm@9663:   "$" => "{\\isachardollar}" |
wenzelm@9663:   "%" => "{\\isacharpercent}" |
wenzelm@9663:   "&" => "{\\isacharampersand}" |
wenzelm@9663:   "'" => "{\\isacharprime}" |
wenzelm@9663:   "(" => "{\\isacharparenleft}" |
wenzelm@9663:   ")" => "{\\isacharparenright}" |
wenzelm@9663:   "*" => "{\\isacharasterisk}" |
wenzelm@9668:   "+" => "{\\isacharplus}" |
wenzelm@9668:   "," => "{\\isacharcomma}" |
wenzelm@9663:   "-" => "{\\isacharminus}" |
wenzelm@9668:   "." => "{\\isachardot}" |
wenzelm@9668:   "/" => "{\\isacharslash}" |
wenzelm@9668:   ":" => "{\\isacharcolon}" |
wenzelm@9668:   ";" => "{\\isacharsemicolon}" |
wenzelm@9663:   "<" => "{\\isacharless}" |
wenzelm@9668:   "=" => "{\\isacharequal}" |
wenzelm@9663:   ">" => "{\\isachargreater}" |
wenzelm@9668:   "?" => "{\\isacharquery}" |
wenzelm@9668:   "@" => "{\\isacharat}" |
wenzelm@9663:   "[" => "{\\isacharbrackleft}" |
wenzelm@9663:   "\\" => "{\\isacharbackslash}" |
wenzelm@9663:   "]" => "{\\isacharbrackright}" |
wenzelm@9663:   "^" => "{\\isacharcircum}" |
wenzelm@9663:   "_" => "{\\isacharunderscore}" |
wenzelm@9668:   "`" => "{\\isacharbackquote}" |
wenzelm@9663:   "{" => "{\\isacharbraceleft}" |
wenzelm@9663:   "|" => "{\\isacharbar}" |
wenzelm@9663:   "}" => "{\\isacharbraceright}" |
wenzelm@9663:   "~" => "{\\isachartilde}" |
wenzelm@14992:   c => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c;
wenzelm@7726: 
wenzelm@14924: val output_chrs = translate_string output_chr;
wenzelm@14924: 
wenzelm@14924: fun output_known_sym (known_sym, known_ctrl) sym =
wenzelm@14874:   (case Symbol.decode sym of
wenzelm@14874:     Symbol.Char s => output_chr s
wenzelm@14924:   | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
wenzelm@14924:   | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
wenzelm@14874:   | Symbol.Raw s => s);
wenzelm@7900: 
wenzelm@7900: in
wenzelm@7900: 
wenzelm@14924: val output_known_symbols = implode oo (map o output_known_sym);
wenzelm@14924: val output_symbols = output_known_symbols (K true, K true);
wenzelm@8192: val output_syms = output_symbols o Symbol.explode;
wenzelm@7900: 
wenzelm@22648: val output_syms_antiqs =
wenzelm@22648:   Antiquote.scan_antiquotes #> map
wenzelm@22648:   (fn Antiquote.Text s => output_syms s
wenzelm@22648:     | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)) #>
wenzelm@22648:   implode;
wenzelm@22648: 
wenzelm@7900: end;
wenzelm@7726: 
wenzelm@7726: 
wenzelm@7726: (* token output *)
wenzelm@7726: 
wenzelm@7726: structure T = OuterLex;
wenzelm@7726: 
wenzelm@7756: val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
wenzelm@7756: 
wenzelm@17081: fun output_basic tok =
wenzelm@17081:   let val s = T.val_of tok in
wenzelm@17081:     if invisible_token tok then ""
wenzelm@17081:     else if T.is_kind T.Command tok then
wenzelm@17081:       "\\isacommand{" ^ output_syms s ^ "}"
wenzelm@17081:     else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
wenzelm@17081:       "\\isakeyword{" ^ output_syms s ^ "}"
wenzelm@17169:     else if T.is_kind T.String tok then
wenzelm@17169:       enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
wenzelm@17169:     else if T.is_kind T.AltString tok then
wenzelm@17169:       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
wenzelm@17186:     else if T.is_kind T.Verbatim tok then
wenzelm@22648:       enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
wenzelm@22648:         (output_syms_antiqs (s, T.position_of tok))
wenzelm@17081:     else output_syms s
wenzelm@17081:   end;
wenzelm@17081: 
wenzelm@17081: fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n";
wenzelm@7745: 
wenzelm@17081: fun output_markup_env cmd txt =
wenzelm@17081:   "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
wenzelm@17081:   Symbol.strip_blanks txt ^
wenzelm@17081:   "%\n\\end{isamarkup" ^ cmd ^ "}%\n";
wenzelm@7756: 
wenzelm@17081: fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
wenzelm@7726: 
wenzelm@17081: val markup_true = "\\isamarkuptrue%\n";
wenzelm@17081: val markup_false = "\\isamarkupfalse%\n";
wenzelm@7726: 
wenzelm@17081: val begin_delim = enclose "%\n\\isadelim" "\n";
wenzelm@17081: val end_delim = enclose "%\n\\endisadelim" "\n";
wenzelm@17081: val begin_tag = enclose "%\n\\isatag" "\n";
wenzelm@17081: fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
wenzelm@11860: 
wenzelm@11860: 
wenzelm@7726: (* theory presentation *)
wenzelm@7726: 
wenzelm@9707: val tex_trailer =
wenzelm@9707:   "%%% Local Variables:\n\
wenzelm@9135:   \%%% mode: latex\n\
wenzelm@9135:   \%%% TeX-master: \"root\"\n\
wenzelm@9144:   \%%% End:\n";
wenzelm@8192: 
wenzelm@9916: fun isabelle_file name txt =
wenzelm@9916:   "%\n\\begin{isabellebody}%\n\
wenzelm@10247:   \\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
wenzelm@9916:   "\\end{isabellebody}%\n" ^ tex_trailer;
wenzelm@9707: 
wenzelm@14924: fun symbol_source known name syms = isabelle_file name
wenzelm@14924:   ("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
wenzelm@14924:     output_known_symbols known syms);
wenzelm@7726: 
wenzelm@9038: fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
wenzelm@7726: 
wenzelm@7726: 
wenzelm@8460: (* print mode *)
wenzelm@8460: 
wenzelm@8965: val latexN = "latex";
wenzelm@17218: val modes = [latexN, Symbol.xsymbolsN];
wenzelm@8965: 
wenzelm@8460: fun latex_output str =
wenzelm@8460:   let val syms = Symbol.explode str
wenzelm@23621:   in (output_symbols syms, Symbol.length syms) end;
wenzelm@19265: 
wenzelm@23621: fun latex_markup (s, _) =
wenzelm@23621:   if s = Markup.keywordN then ("\\isakeyword{", "}")
wenzelm@23621:   else if s = Markup.commandN then ("\\isacommand{", "}")
wenzelm@23621:   else ("", "");
wenzelm@10955: 
wenzelm@23621: fun latex_indent "" _ = ""
wenzelm@23621:   | latex_indent s _ = enclose "\\isaindent{" "}" s;
wenzelm@23621: 
wenzelm@23621: val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
wenzelm@23703: val _ = Markup.add_mode latexN latex_markup;
wenzelm@23703: val _ = Pretty.add_mode latexN latex_indent;
wenzelm@8460: 
wenzelm@7726: end;