(* Title: Pure/Thy/latex.ML
Author: Markus Wenzel, TU Muenchen
LaTeX presentation elements -- based on outer lexical syntax.
*)
signature LATEX =
sig
val output_known_symbols: (string -> bool) * (string -> bool) ->
Symbol.symbol list -> string
val output_symbols: Symbol.symbol list -> string
val output_basic: Token.T -> string
val output_markup: string -> string -> string
val output_markup_env: string -> string -> string
val output_verbatim: string -> string
val markup_true: string
val markup_false: string
val begin_delim: string -> string
val end_delim: string -> string
val begin_tag: string -> string
val end_tag: string -> string
val tex_trailer: string
val isabelle_file: string -> string -> string
val symbol_source: (string -> bool) * (string -> bool) ->
string -> Symbol.symbol list -> string
val theory_entry: string -> string
val modes: string list
end;
structure Latex: LATEX =
struct
(* literal text *)
local
val hex = Int.fmt StringCvt.HEX;
fun hex_byte c = hex (ord c div 16) ^ hex (ord c mod 16);
in
fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}";
fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg);
end;
(* symbol output *)
local
val char_table =
Symtab.make
[("!", "{\\isacharbang}"),
("\"", "{\\isachardoublequote}"),
("#", "{\\isacharhash}"),
("$", "{\\isachardollar}"),
("%", "{\\isacharpercent}"),
("&", "{\\isacharampersand}"),
("'", "{\\isacharprime}"),
("(", "{\\isacharparenleft}"),
(")", "{\\isacharparenright}"),
("*", "{\\isacharasterisk}"),
("+", "{\\isacharplus}"),
(",", "{\\isacharcomma}"),
("-", "{\\isacharminus}"),
(".", "{\\isachardot}"),
("/", "{\\isacharslash}"),
(":", "{\\isacharcolon}"),
(";", "{\\isacharsemicolon}"),
("<", "{\\isacharless}"),
("=", "{\\isacharequal}"),
(">", "{\\isachargreater}"),
("?", "{\\isacharquery}"),
("@", "{\\isacharat}"),
("[", "{\\isacharbrackleft}"),
("\\", "{\\isacharbackslash}"),
("]", "{\\isacharbrackright}"),
("^", "{\\isacharcircum}"),
("_", "{\\isacharunderscore}"),
("`", "{\\isacharbackquote}"),
("{", "{\\isacharbraceleft}"),
("|", "{\\isacharbar}"),
("}", "{\\isacharbraceright}"),
("~", "{\\isachartilde}")];
fun output_chr " " = "\\ "
| output_chr "\n" = "\\isanewline\n"
| output_chr c =
(case Symtab.lookup char_table c of
SOME s => enclose_literal c s
| NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
val output_chrs = translate_string output_chr;
fun output_known_sym (known_sym, known_ctrl) sym =
(case Symbol.decode sym of
Symbol.Char s => output_chr s
| Symbol.UTF8 s => s
| Symbol.Sym s =>
if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s)
else output_chrs sym
| Symbol.Ctrl s =>
if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
else output_chrs sym
| Symbol.Raw s => s);
in
val output_known_symbols = implode oo (map o output_known_sym);
val output_symbols = output_known_symbols (K true, K true);
val output_syms = output_symbols o Symbol.explode;
val output_syms_antiq =
(fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
| Antiquote.Antiq (ss, _) =>
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
(output_symbols (map Symbol_Pos.symbol ss))
| Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}"
| Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}");
end;
(* token output *)
val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment;
fun output_basic tok =
let val s = Token.content_of tok in
if invisible_token tok then ""
else if Token.is_kind Token.Command tok then
"\\isacommand{" ^ output_syms s ^ "}"
else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
"\\isakeyword{" ^ output_syms s ^ "}"
else if Token.is_kind Token.String tok then
output_syms s |> enclose
(enclose_literal "\"" "{\\isachardoublequoteopen}")
(enclose_literal "\"" "{\\isachardoublequoteclose}")
else if Token.is_kind Token.AltString tok then
output_syms s |> enclose
(enclose_literal "`" "{\\isacharbackquoteopen}")
(enclose_literal "`" "{\\isacharbackquoteclose}")
else if Token.is_kind Token.Verbatim tok then
let
val (txt, pos) = Token.source_position_of tok;
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
in
out |> enclose
(enclose_literal "{*" "{\\isacharverbatimopen}")
(enclose_literal "*}" "{\\isacharverbatimclose}")
end
else output_syms s
end;
fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n";
fun output_markup_env cmd txt =
"%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
Symbol.strip_blanks txt ^
"%\n\\end{isamarkup" ^ cmd ^ "}%\n";
fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
val markup_true = "\\isamarkuptrue%\n";
val markup_false = "\\isamarkupfalse%\n";
val begin_delim = enclose "%\n\\isadelim" "\n";
val end_delim = enclose "%\n\\endisadelim" "\n";
val begin_tag = enclose "%\n\\isatag" "\n";
fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
(* theory presentation *)
val tex_trailer =
"%%% Local Variables:\n\
\%%% mode: latex\n\
\%%% TeX-master: \"root\"\n\
\%%% End:\n";
fun isabelle_file name txt =
"%\n\\begin{isabellebody}%\n\
\\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
"\\end{isabellebody}%\n" ^ tex_trailer;
fun symbol_source known name syms = isabelle_file name
("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
output_known_symbols known syms);
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
(* print mode *)
val latexN = "latex";
val modes = [latexN, Symbol.xsymbolsN];
fun latex_output str =
let val syms = Symbol.explode str
in (output_symbols syms, Symbol.length syms) end;
fun latex_markup (s, _) =
if s = Markup.keywordN then ("\\isakeyword{", "}")
else if s = Markup.commandN then ("\\isacommand{", "}")
else Markup.no_output;
fun latex_indent "" _ = ""
| latex_indent s _ = enclose "\\isaindent{" "}" s;
val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
val _ = Markup.add_mode latexN latex_markup;
val _ = Pretty.add_mode latexN latex_indent;
end;