src/Pure/Thy/latex.ML
changeset 69346 3c29edccf739
parent 67462 c23d9375e661
child 71899 9a12eb655f67
equal deleted inserted replaced
69345:6bd63c94cf62 69346:3c29edccf739
    27   val environment_block: string -> text list -> text
    27   val environment_block: string -> text list -> text
    28   val environment: string -> string -> string
    28   val environment: string -> string -> string
    29   val isabelle_body: string -> text list -> text list
    29   val isabelle_body: string -> text list -> text list
    30   val theory_entry: string -> string
    30   val theory_entry: string -> string
    31   val latexN: string
    31   val latexN: string
       
    32   val latex_output: string -> string * int
       
    33   val latex_markup: string * Properties.T -> Markup.output
       
    34   val latex_indent: string -> int -> string
    32 end;
    35 end;
    33 
    36 
    34 structure Latex: LATEX =
    37 structure Latex: LATEX =
    35 struct
    38 struct
    36 
    39 
   239 
   242 
   240 fun latex_output str =
   243 fun latex_output str =
   241   let val syms = Symbol.explode str
   244   let val syms = Symbol.explode str
   242   in (output_symbols syms, length_symbols syms) end;
   245   in (output_symbols syms, length_symbols syms) end;
   243 
   246 
   244 fun latex_markup (s, _) =
   247 fun latex_markup (s, _: Properties.T) =
   245   if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
   248   if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
   246   then ("\\isacommand{", "}")
   249   then ("\\isacommand{", "}")
   247   else if s = Markup.keyword2N
   250   else if s = Markup.keyword2N
   248   then ("\\isakeyword{", "}")
   251   then ("\\isakeyword{", "}")
   249   else Markup.no_output;
   252   else Markup.no_output;