--- 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;
--- 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)