--- a/src/Pure/Thy/latex.ML Sun Oct 21 19:36:12 2001 +0200
+++ b/src/Pure/Thy/latex.ML Sun Oct 21 19:40:39 2001 +0200
@@ -11,6 +11,7 @@
val output_symbols: Symbol.symbol list -> string
datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
val output_tokens: (token * string) list -> string
+ val flag_markup: bool -> string
val tex_trailer: string
val isabelle_file: string -> string -> string
val old_symbol_source: string -> Symbol.symbol list -> string
@@ -114,6 +115,10 @@
val output_tokens = implode o map output_tok;
+fun flag_markup true = "\\isamarkuptrue%\n"
+ | flag_markup false = "\\isamarkupfalse%\n";
+
+
(* theory presentation *)
val tex_trailer =