token translation: enclose "\\mbox{" "}";
authorwenzelm
Tue Aug 08 16:57:44 2000 +0200 (2000-08-08)
changeset 95588d5221bf765b
parent 9557 c1e730bebcaa
child 9559 1f99296758c2
token translation: enclose "\\mbox{" "}";
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Tue Aug 08 16:39:34 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Aug 08 16:57:44 2000 +0200
     1.3 @@ -121,7 +121,9 @@
     1.4    let val syms = Symbol.explode str
     1.5    in (output_symbols syms, real (Symbol.length syms)) end;
     1.6  
     1.7 -val token_translation = map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
     1.8 +val token_translation =
     1.9 +  map (fn s => (latexN, s, apfst (enclose "\\mbox{" "}") o latex_output))
    1.10 +    Syntax.standard_token_classes;
    1.11  
    1.12  val _ = Symbol.add_mode latexN latex_output;
    1.13  val setup = [Theory.add_tokentrfuns token_translation];