--- a/src/Pure/Thy/latex.ML Mon Aug 28 20:32:38 2000 +0200
+++ b/src/Pure/Thy/latex.ML Mon Aug 28 20:32:55 2000 +0200
@@ -10,6 +10,7 @@
sig
datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
val output_tokens: (token * string) list -> string
+ val tex_trailer: string
val isabelle_file: string -> string
val old_symbol_source: string -> Symbol.symbol list -> string
val theory_entry: string -> string
@@ -117,14 +118,15 @@
(* theory presentation *)
-val isabelle_file = enclose
- "\\begin{isabelle}%\n"
- "\\end{isabelle}%\n\
- \%%% Local Variables:\n\
+val tex_trailer =
+ "%%% Local Variables:\n\
\%%% mode: latex\n\
\%%% TeX-master: \"root\"\n\
\%%% End:\n";
+val isabelle_file =
+ enclose "%\n\\begin{isabellebody}%\n" ("\\end{isabellebody}%\n" ^ tex_trailer);
+
fun old_symbol_source name syms =
isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);