equal
deleted
inserted
replaced
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 |