define \isabellecontext;
authorwenzelm
Mon Sep 11 17:37:09 2000 +0200 (2000-09-11)
changeset 99164a703366494b
parent 9915 8de4ea6de3d0
child 9917 5af7632388a0
define \isabellecontext;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Mon Sep 11 17:35:50 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Mon Sep 11 17:37:09 2000 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
     1.5    val output_tokens: (token * string) list -> string
     1.6    val tex_trailer: string
     1.7 -  val isabelle_file: string -> string
     1.8 +  val isabelle_file: string -> string -> string
     1.9    val old_symbol_source: string -> Symbol.symbol list -> string
    1.10    val theory_entry: string -> string
    1.11    val modes: string list
    1.12 @@ -124,11 +124,13 @@
    1.13    \%%% TeX-master: \"root\"\n\
    1.14    \%%% End:\n";
    1.15  
    1.16 -val isabelle_file =
    1.17 -  enclose "%\n\\begin{isabellebody}%\n" ("\\end{isabellebody}%\n" ^ tex_trailer);
    1.18 +fun isabelle_file name txt =
    1.19 +  "%\n\\begin{isabellebody}%\n\
    1.20 +  \\\def\\isabellecontext{" ^ name ^ "}%\n" ^ txt ^
    1.21 +  "\\end{isabellebody}%\n" ^ tex_trailer;
    1.22  
    1.23  fun old_symbol_source name syms =
    1.24 -  isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
    1.25 +  isabelle_file name ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
    1.26  
    1.27  fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
    1.28