# HG changeset patch
# User wenzelm
# Date 1159386835 -7200
# Node ID 2233f6afc491aeca5d0cff3c464207959048a71b
# Parent  c8fdad2dc6e6798820c5bcd3fe6edc62405e861c
reverted to 1.58;

diff -r c8fdad2dc6e6 -r 2233f6afc491 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Wed Sep 27 21:49:34 2006 +0200
+++ b/src/Pure/Thy/html.ML	Wed Sep 27 21:53:55 2006 +0200
@@ -204,9 +204,10 @@
   val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;
 
   fun output_sym s =
-    (case Symtab.lookup html_syms s of
-      SOME x => x
-    | NONE => (real (size s), translate_string escape s));
+    if Symbol.is_raw s then (1.0, Symbol.decode_raw s)
+    else
+      (case Symtab.lookup html_syms s of SOME x => x
+      | NONE => (real (size s), translate_string escape s));
 
   fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
   fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);