more flexibile \setisabellecontext, independently of header;
authorwenzelm
Sun Nov 02 16:09:35 2014 +0100 (2014-11-02)
changeset 58870e2c0d8ef29cb
parent 58869 963fd2084e8f
child 58871 c399ae4b836f
more flexibile \setisabellecontext, independently of header;
lib/texinputs/draft.tex
lib/texinputs/isabelle.sty
src/Pure/Thy/latex.ML
src/Pure/Thy/present.ML
     1.1 --- a/lib/texinputs/draft.tex	Sun Nov 02 16:05:43 2014 +0100
     1.2 +++ b/lib/texinputs/draft.tex	Sun Nov 02 16:09:35 2014 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  \usepackage{textcomp}
     1.5  
     1.6  \pagestyle{myheadings}
     1.7 -\renewcommand{\isamarkupheader}[1]%
     1.8 +\newcommand{\isamarkupfile}[1]%
     1.9  {{\def\isacharunderscore{\mbox{-}}%
    1.10  \section*{#1}\markright{FILE~``\isabellecontext''}}}
    1.11  
     2.1 --- a/lib/texinputs/isabelle.sty	Sun Nov 02 16:05:43 2014 +0100
     2.2 +++ b/lib/texinputs/isabelle.sty	Sun Nov 02 16:09:35 2014 +0100
     2.3 @@ -7,6 +7,7 @@
     2.4  % isabelle environments
     2.5  
     2.6  \newcommand{\isabellecontext}{UNKNOWN}
     2.7 +\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
     2.8  
     2.9  \newcommand{\isastyle}{\UNDEF}
    2.10  \newcommand{\isastylett}{\UNDEF}
     3.1 --- a/src/Pure/Thy/latex.ML	Sun Nov 02 16:05:43 2014 +0100
     3.2 +++ b/src/Pure/Thy/latex.ML	Sun Nov 02 16:09:35 2014 +0100
     3.3 @@ -21,7 +21,7 @@
     3.4    val begin_tag: string -> string
     3.5    val end_tag: string -> string
     3.6    val tex_trailer: string
     3.7 -  val isabelle_file: string -> string -> string
     3.8 +  val isabelle_theory: string -> string -> string
     3.9    val symbol_source: (string -> bool) * (string -> bool) ->
    3.10      string -> Symbol.symbol list -> string
    3.11    val theory_entry: string -> string
    3.12 @@ -167,14 +167,15 @@
    3.13    \%%% TeX-master: \"root\"\n\
    3.14    \%%% End:\n";
    3.15  
    3.16 -fun isabelle_file name txt =
    3.17 +fun isabelle_theory name txt =
    3.18    "%\n\\begin{isabellebody}%\n\
    3.19 -  \\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
    3.20 +  \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
    3.21    "\\end{isabellebody}%\n" ^ tex_trailer;
    3.22  
    3.23 -fun symbol_source known name syms = isabelle_file name
    3.24 -  ("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
    3.25 -    output_known_symbols known syms);
    3.26 +fun symbol_source known name syms =
    3.27 +  isabelle_theory name
    3.28 +    ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
    3.29 +      output_known_symbols known syms);
    3.30  
    3.31  fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
    3.32  
     4.1 --- a/src/Pure/Thy/present.ML	Sun Nov 02 16:05:43 2014 +0100
     4.2 +++ b/src/Pure/Thy/present.ML	Sun Nov 02 16:09:35 2014 +0100
     4.3 @@ -369,7 +369,7 @@
     4.4  
     4.5  fun theory_output name s =
     4.6    with_session_info () (fn _ =>
     4.7 -    change_theory_info name (fn (_, html_source) => (Latex.isabelle_file name s, html_source)));
     4.8 +    change_theory_info name (fn (_, html_source) => (Latex.isabelle_theory name s, html_source)));
     4.9  
    4.10  fun begin_theory update_time mk_text thy =
    4.11    with_session_info thy (fn {name = session_name, chapter, ...} =>