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@9135:   datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
wenzelm@9135:   val output_tokens: (token * string) list -> string
wenzelm@11860:   val flag_markup: bool -> 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@7900: end;
wenzelm@7726: 
wenzelm@7726: 
wenzelm@7726: (* token output *)
wenzelm@7726: 
wenzelm@7726: structure T = OuterLex;
wenzelm@7726: 
wenzelm@8660: datatype token =
wenzelm@8660:   Basic of T.token |
wenzelm@9135:   Markup of string |
wenzelm@9135:   MarkupEnv of string |
wenzelm@9135:   Verbatim;
wenzelm@7756: 
wenzelm@7756: 
wenzelm@7756: val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
wenzelm@7756: 
wenzelm@9135: fun output_tok (Basic tok, _) =
wenzelm@7752:       let val s = T.val_of tok in
wenzelm@7756:         if invisible_token tok then ""
wenzelm@7800:         else if T.is_kind T.Command tok then
wenzelm@9668:           "\\isacommand{" ^ output_syms s ^ "}"
wenzelm@14680:         else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
wenzelm@7900:           "\\isakeyword{" ^ output_syms s ^ "}"
berghofe@14598:         else if T.is_kind T.String tok then output_syms (Library.quote s)
wenzelm@7900:         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
wenzelm@7900:         else output_syms s
wenzelm@7756:       end
wenzelm@11012:   | output_tok (Markup cmd, txt) =
wenzelm@11012:       "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"
wenzelm@9135:   | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
wenzelm@11012:       Symbol.strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
wenzelm@11012:   | output_tok (Verbatim, txt) = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
wenzelm@7745: 
wenzelm@7756: 
wenzelm@7756: val output_tokens = implode o map output_tok;
wenzelm@7726: 
wenzelm@7726: 
wenzelm@11860: fun flag_markup true = "\\isamarkuptrue%\n"
wenzelm@11860:   | flag_markup false = "\\isamarkupfalse%\n";
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@9135: val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN];
wenzelm@8965: 
wenzelm@8460: fun latex_output str =
wenzelm@8460:   let val syms = Symbol.explode str
wenzelm@8460:   in (output_symbols syms, real (Symbol.length syms)) end;
wenzelm@8460: 
wenzelm@10955: fun latex_indent "" = ""
wenzelm@10955:   | latex_indent s = enclose "\\isaindent{" "}" s;
wenzelm@10955: 
wenzelm@14973: val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.encode_raw);
wenzelm@8460: 
wenzelm@8460: 
wenzelm@7726: end;