src/Pure/Thy/latex.ML
changeset 11860 36ba0d4a836c
parent 11719 49c14348a42b
child 14361 ad2f5da643b4
     1.1 --- a/src/Pure/Thy/latex.ML	Sun Oct 21 19:36:12 2001 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Sun Oct 21 19:40:39 2001 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val output_symbols: Symbol.symbol list -> string
     1.5    datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
     1.6    val output_tokens: (token * string) list -> string
     1.7 +  val flag_markup: bool -> string
     1.8    val tex_trailer: string
     1.9    val isabelle_file: string -> string -> string
    1.10    val old_symbol_source: string -> Symbol.symbol list -> string
    1.11 @@ -114,6 +115,10 @@
    1.12  val output_tokens = implode o map output_tok;
    1.13  
    1.14  
    1.15 +fun flag_markup true = "\\isamarkuptrue%\n"
    1.16 +  | flag_markup false = "\\isamarkupfalse%\n";
    1.17 +
    1.18 +
    1.19  (* theory presentation *)
    1.20  
    1.21  val tex_trailer =