# HG changeset patch
# User wenzelm
# Date 1414940975 -3600
# Node ID e2c0d8ef29cbe78dac32e24c35dc12445bea4373
# Parent  963fd2084e8fc04ffa03ef424b40356fdeb39c98
more flexibile \setisabellecontext, independently of header;

diff -r 963fd2084e8f -r e2c0d8ef29cb lib/texinputs/draft.tex
--- a/lib/texinputs/draft.tex	Sun Nov 02 16:05:43 2014 +0100
+++ b/lib/texinputs/draft.tex	Sun Nov 02 16:09:35 2014 +0100
@@ -10,7 +10,7 @@
 \usepackage{textcomp}
 
 \pagestyle{myheadings}
-\renewcommand{\isamarkupheader}[1]%
+\newcommand{\isamarkupfile}[1]%
 {{\def\isacharunderscore{\mbox{-}}%
 \section*{#1}\markright{FILE~``\isabellecontext''}}}
 
diff -r 963fd2084e8f -r e2c0d8ef29cb lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Sun Nov 02 16:05:43 2014 +0100
+++ b/lib/texinputs/isabelle.sty	Sun Nov 02 16:09:35 2014 +0100
@@ -7,6 +7,7 @@
 % isabelle environments
 
 \newcommand{\isabellecontext}{UNKNOWN}
+\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
 
 \newcommand{\isastyle}{\UNDEF}
 \newcommand{\isastylett}{\UNDEF}
diff -r 963fd2084e8f -r e2c0d8ef29cb src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Nov 02 16:05:43 2014 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Nov 02 16:09:35 2014 +0100
@@ -21,7 +21,7 @@
   val begin_tag: string -> string
   val end_tag: string -> string
   val tex_trailer: string
-  val isabelle_file: string -> string -> string
+  val isabelle_theory: string -> string -> string
   val symbol_source: (string -> bool) * (string -> bool) ->
     string -> Symbol.symbol list -> string
   val theory_entry: string -> string
@@ -167,14 +167,15 @@
   \%%% TeX-master: \"root\"\n\
   \%%% End:\n";
 
-fun isabelle_file name txt =
+fun isabelle_theory name txt =
   "%\n\\begin{isabellebody}%\n\
-  \\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
+  \\\setisabellecontext{" ^ 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 symbol_source known name syms =
+  isabelle_theory name
+    ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
+      output_known_symbols known syms);
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
 
diff -r 963fd2084e8f -r e2c0d8ef29cb src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Nov 02 16:05:43 2014 +0100
+++ b/src/Pure/Thy/present.ML	Sun Nov 02 16:09:35 2014 +0100
@@ -369,7 +369,7 @@
 
 fun theory_output name s =
   with_session_info () (fn _ =>
-    change_theory_info name (fn (_, html_source) => (Latex.isabelle_file name s, html_source)));
+    change_theory_info name (fn (_, html_source) => (Latex.isabelle_theory name s, html_source)));
 
 fun begin_theory update_time mk_text thy =
   with_session_info thy (fn {name = session_name, chapter, ...} =>