# HG changeset patch
# User wenzelm
# Date 1087890683 -7200
# Node ID a16bc5abad45453a53af9343bbabf63d42bba502
# Parent  26fb63c4acb5f6d116ee413a1e770c10ae7c681b
tuned output;

diff -r 26fb63c4acb5 -r a16bc5abad45 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Mon Jun 21 16:49:58 2004 +0200
+++ b/src/Pure/Thy/html.ML	Tue Jun 22 09:51:23 2004 +0200
@@ -225,8 +225,8 @@
 in
 
 fun output_width str =
-  if not (exists_string (equal "<" orf equal ">" orf equal "&") str)
-  then (str, real (size str))
+  if not (exists_string (equal "\\" orf equal "<" orf equal ">" orf equal "&") str)
+  then Symbol.default_output str
   else
     let val (width, syms) = foldl_map add_sym (0.0, map output_sym (Symbol.explode str))
     in (implode (scripts syms), width) end;
diff -r 26fb63c4acb5 -r a16bc5abad45 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Jun 21 16:49:58 2004 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Jun 22 09:51:23 2004 +0200
@@ -64,7 +64,7 @@
   "|" => "{\\isacharbar}" |
   "}" => "{\\isacharbraceright}" |
   "~" => "{\\isachartilde}" |
-  c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c;
+  c => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c;
 
 val output_chrs = translate_string output_chr;
 
diff -r 26fb63c4acb5 -r a16bc5abad45 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Mon Jun 21 16:49:58 2004 +0200
+++ b/src/Pure/proof_general.ML	Tue Jun 22 09:51:23 2004 +0200
@@ -48,10 +48,11 @@
   | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
 
 fun xsymbols_output s =
-  if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
+  if Symbol.chars_only s then Symbol.default_output s
+  else if Output.has_mode xsymbolsN then
     let val syms = Symbol.explode s
     in (implode (map xsym_output syms), real (Symbol.length syms)) end
-  else Symbol.default_output s;
+  else Symbol.symbol_output s;
 
 fun pgml_output (s, len) =
   if pgml () then (XML.text s, len)