src/Pure/Thy/latex.ML
changeset 8499 8958ece3bbdf
parent 8460 274426d1adbc
child 8660 e5048a26e1d8
     1.1 --- a/src/Pure/Thy/latex.ML	Fri Mar 17 16:30:03 2000 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Fri Mar 17 16:30:45 2000 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature LATEX =
     1.5  sig
     1.6    datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
     1.7 -  val old_symbol_source: Symbol.symbol list -> string
     1.8 +  val old_symbol_source: string -> Symbol.symbol list -> string
     1.9    val token_source: token list -> string
    1.10    val theory_entry: string -> string
    1.11  end;
    1.12 @@ -90,7 +90,9 @@
    1.13  
    1.14  val isabelle_env = enclose "\\begin{isabelle}%\n" "\\end{isabelle}%\n";
    1.15  
    1.16 -val old_symbol_source = isabelle_env o output_symbols;
    1.17 +fun old_symbol_source name syms =
    1.18 +  isabelle_env ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
    1.19 +
    1.20  val token_source = isabelle_env o output_tokens;
    1.21  
    1.22  fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";