src/Pure/Thy/latex.ML
changeset 11719 49c14348a42b
parent 11012 8eb472444705
child 11860 36ba0d4a836c
equal deleted inserted replaced
11718:92706a69dacc 11719:49c14348a42b
     6 LaTeX presentation primitives (based on outer lexical syntax).
     6 LaTeX presentation primitives (based on outer lexical syntax).
     7 *)
     7 *)
     8 
     8 
     9 signature LATEX =
     9 signature LATEX =
    10 sig
    10 sig
       
    11   val output_symbols: Symbol.symbol list -> string
    11   datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
    12   datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
    12   val output_tokens: (token * string) list -> string
    13   val output_tokens: (token * string) list -> string
    13   val tex_trailer: string
    14   val tex_trailer: string
    14   val isabelle_file: string -> string -> string
    15   val isabelle_file: string -> string -> string
    15   val old_symbol_source: string -> Symbol.symbol list -> string
    16   val old_symbol_source: string -> Symbol.symbol list -> string