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