src/Pure/Thy/latex.ML
changeset 9558 8d5221bf765b
parent 9505 09c75c801dde
child 9663 e4d58f1be05b
equal deleted inserted replaced
9557:c1e730bebcaa 9558:8d5221bf765b
   119 
   119 
   120 fun latex_output str =
   120 fun latex_output str =
   121   let val syms = Symbol.explode str
   121   let val syms = Symbol.explode str
   122   in (output_symbols syms, real (Symbol.length syms)) end;
   122   in (output_symbols syms, real (Symbol.length syms)) end;
   123 
   123 
   124 val token_translation = map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
   124 val token_translation =
       
   125   map (fn s => (latexN, s, apfst (enclose "\\mbox{" "}") o latex_output))
       
   126     Syntax.standard_token_classes;
   125 
   127 
   126 val _ = Symbol.add_mode latexN latex_output;
   128 val _ = Symbol.add_mode latexN latex_output;
   127 val setup = [Theory.add_tokentrfuns token_translation];
   129 val setup = [Theory.add_tokentrfuns token_translation];
   128 
   130 
   129 
   131