added tex_trailer;
authorwenzelm
Mon Aug 28 20:32:55 2000 +0200 (2000-08-28)
changeset 9707067c25edd1bd
parent 9706 8e48a19fc81e
child 9708 5f21379beb87
added tex_trailer;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Mon Aug 28 20:32:38 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Mon Aug 28 20:32:55 2000 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  sig
     1.5    datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
     1.6    val output_tokens: (token * string) list -> string
     1.7 +  val tex_trailer: string
     1.8    val isabelle_file: string -> string
     1.9    val old_symbol_source: string -> Symbol.symbol list -> string
    1.10    val theory_entry: string -> string
    1.11 @@ -117,14 +118,15 @@
    1.12  
    1.13  (* theory presentation *)
    1.14  
    1.15 -val isabelle_file = enclose
    1.16 -  "\\begin{isabelle}%\n"
    1.17 -  "\\end{isabelle}%\n\
    1.18 -  \%%% Local Variables:\n\
    1.19 +val tex_trailer =
    1.20 +  "%%% Local Variables:\n\
    1.21    \%%% mode: latex\n\
    1.22    \%%% TeX-master: \"root\"\n\
    1.23    \%%% End:\n";
    1.24  
    1.25 +val isabelle_file =
    1.26 +  enclose "%\n\\begin{isabellebody}%\n" ("\\end{isabellebody}%\n" ^ tex_trailer);
    1.27 +
    1.28  fun old_symbol_source name syms =
    1.29    isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
    1.30