1.1 --- a/src/Pure/Syntax/token_trans.ML	Sun Jun 06 18:35:11 2004 +0200
     1.2 +++ b/src/Pure/Syntax/token_trans.ML	Sun Jun 06 18:35:26 2004 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  val cyan = "\^[[36m";
     1.5  val white = "\^[[37m";
     1.6  
     1.7 -fun style (ref s) x = (s ^ x ^ normal, real (size x));
     1.8 +fun style (ref s) x = Output.output_width x |> apfst (enclose s normal);
     1.9  
    1.10  
    1.11  (* print modes "xterm" and "xterm_color" *)
    1.12 @@ -116,7 +116,7 @@
    1.13  (** standard token translations **)
    1.14  
    1.15  val token_translation =
    1.16 -  map (fn s => ("", s, fn x => (x, real (size x)))) standard_token_classes @
    1.17 +  map (fn s => ("", s, Output.output_width)) standard_token_classes @
    1.18    xterm_trans;
    1.19  
    1.20  

     2.1 --- a/src/Pure/proof_general.ML	Sun Jun 06 18:35:11 2004 +0200
     2.2 +++ b/src/Pure/proof_general.ML	Sun Jun 06 18:35:26 2004 +0200
     2.3 @@ -51,7 +51,7 @@
     2.4    if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
     2.5      let val syms = Symbol.explode s
     2.6      in (implode (map xsym_output syms), real (Symbol.length syms)) end
     2.7 -  else (s, real (size s));
     2.8 +  else Symbol.default_output s;
     2.9  
    2.10  fun pgml_output (s, len) =
    2.11    if pgml () then (XML.text s, len)