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