# HG changeset patch
# User wenzelm
# Date 1086539726 -7200
# Node ID 7586233bd4bdf06008cb8d851064b85f66872309
# Parent  8989eedf72a1919b115151ad9305e3cb7cda6f24
Symbol.output;

diff -r 8989eedf72a1 -r 7586233bd4bd src/Pure/Syntax/token_trans.ML
--- a/src/Pure/Syntax/token_trans.ML	Sun Jun 06 18:35:11 2004 +0200
+++ b/src/Pure/Syntax/token_trans.ML	Sun Jun 06 18:35:26 2004 +0200
@@ -76,7 +76,7 @@
 val cyan = "\^[[36m";
 val white = "\^[[37m";
 
-fun style (ref s) x = (s ^ x ^ normal, real (size x));
+fun style (ref s) x = Output.output_width x |> apfst (enclose s normal);
 
 
 (* print modes "xterm" and "xterm_color" *)
@@ -116,7 +116,7 @@
 (** standard token translations **)
 
 val token_translation =
-  map (fn s => ("", s, fn x => (x, real (size x)))) standard_token_classes @
+  map (fn s => ("", s, Output.output_width)) standard_token_classes @
   xterm_trans;
 
 
diff -r 8989eedf72a1 -r 7586233bd4bd src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Sun Jun 06 18:35:11 2004 +0200
+++ b/src/Pure/proof_general.ML	Sun Jun 06 18:35:26 2004 +0200
@@ -51,7 +51,7 @@
   if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
     let val syms = Symbol.explode s
     in (implode (map xsym_output syms), real (Symbol.length syms)) end
-  else (s, real (size s));
+  else Symbol.default_output s;
 
 fun pgml_output (s, len) =
   if pgml () then (XML.text s, len)