src/Pure/Thy/latex.ML
changeset 58716 23a380cc45f4
parent 55828 42ac3cfb89f6
child 58727 e3d0a6a012eb
equal deleted inserted replaced
58715:cb8d2470623b 58716:23a380cc45f4
     4 LaTeX presentation elements -- based on outer lexical syntax.
     4 LaTeX presentation elements -- based on outer lexical syntax.
     5 *)
     5 *)
     6 
     6 
     7 signature LATEX =
     7 signature LATEX =
     8 sig
     8 sig
       
     9   val output_ascii: string -> string
     9   val output_known_symbols: (string -> bool) * (string -> bool) ->
    10   val output_known_symbols: (string -> bool) * (string -> bool) ->
    10     Symbol.symbol list -> string
    11     Symbol.symbol list -> string
    11   val output_symbols: Symbol.symbol list -> string
    12   val output_symbols: Symbol.symbol list -> string
    12   val output_basic: Token.T -> string
    13   val output_basic: Token.T -> string
    13   val output_markup: string -> string -> string
    14   val output_markup: string -> string -> string
    27   val modes: string list
    28   val modes: string list
    28 end;
    29 end;
    29 
    30 
    30 structure Latex: LATEX =
    31 structure Latex: LATEX =
    31 struct
    32 struct
       
    33 
       
    34 (* literal ASCII *)
       
    35 
       
    36 val output_ascii =
       
    37   translate_string
       
    38     (fn " " => "\\ "
       
    39       | "\t" => "\\ "
       
    40       | "\n" => "\\isanewline\n"
       
    41       | s =>
       
    42           if exists_string (fn s' => s = s') "#$%^&_{}~\\"
       
    43           then enclose "{\\char`\\" "}" s else s);
       
    44 
    32 
    45 
    33 (* symbol output *)
    46 (* symbol output *)
    34 
    47 
    35 local
    48 local
    36 
    49