# HG changeset patch
# User wenzelm
# Date 1003686039 -7200
# Node ID 36ba0d4a836c1232cb4c32d1c57a8cca9e875a48
# Parent  cb26f392248931f74fdb1ad2845cb76e9dd50a74
flag_markup;

diff -r cb26f3922489 -r 36ba0d4a836c src/Pure/Thy/latex.ML
--- 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 =