wenzelm@7726: (* Title: Pure/Thy/latex.ML wenzelm@7726: ID: $Id$ wenzelm@7726: Author: Markus Wenzel, TU Muenchen wenzelm@8808: License: GPL (GNU GENERAL PUBLIC LICENSE) wenzelm@7726: wenzelm@8460: LaTeX presentation primitives (based on outer lexical syntax). wenzelm@7726: *) wenzelm@7726: wenzelm@7726: signature LATEX = wenzelm@7726: sig 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@9707: val tex_trailer: string wenzelm@9916: val isabelle_file: string -> string -> string wenzelm@8499: val old_symbol_source: string -> Symbol.symbol list -> string wenzelm@7726: val theory_entry: string -> string wenzelm@9135: val modes: string list wenzelm@8965: val setup: (theory -> theory) 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@10184: c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c; wenzelm@7726: wenzelm@7900: fun output_sym s = wenzelm@7900: if size s = 1 then output_chr s wenzelm@7900: else wenzelm@7900: (case explode s of wenzelm@10184: "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " " wenzelm@7973: | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}" wenzelm@7900: | _ => sys_error "output_sym"); wenzelm@7900: wenzelm@7900: in wenzelm@7900: wenzelm@8192: val output_symbols = implode o map output_sym; 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@7800: else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then wenzelm@7900: "\\isakeyword{" ^ output_syms s ^ "}" wenzelm@7900: else if T.is_kind T.String tok then output_syms (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@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@8499: fun old_symbol_source name syms = wenzelm@9916: isabelle_file name ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols 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@9558: val token_translation = wenzelm@9749: map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes; wenzelm@8965: wenzelm@10955: val _ = Symbol.add_mode latexN (latex_output, latex_indent o #1); wenzelm@8965: val setup = [Theory.add_tokentrfuns token_translation]; wenzelm@8460: wenzelm@8460: wenzelm@7726: end;