# HG changeset patch
# User wenzelm
# Date 968686629 -7200
# Node ID 4a703366494bfa45a27749f210cc4c24ba829f37
# Parent  8de4ea6de3d03bf4ae3085a2e63a674fa2ade256
define \isabellecontext;

diff -r 8de4ea6de3d0 -r 4a703366494b src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Sep 11 17:35:50 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Sep 11 17:37:09 2000 +0200
@@ -11,7 +11,7 @@
   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 isabelle_file: string -> string -> string
   val old_symbol_source: string -> Symbol.symbol list -> string
   val theory_entry: string -> string
   val modes: string list
@@ -124,11 +124,13 @@
   \%%% TeX-master: \"root\"\n\
   \%%% End:\n";
 
-val isabelle_file =
-  enclose "%\n\\begin{isabellebody}%\n" ("\\end{isabellebody}%\n" ^ tex_trailer);
+fun isabelle_file name txt =
+  "%\n\\begin{isabellebody}%\n\
+  \\\def\\isabellecontext{" ^ name ^ "}%\n" ^ txt ^
+  "\\end{isabellebody}%\n" ^ tex_trailer;
 
 fun old_symbol_source name syms =
-  isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
+  isabelle_file name ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";