# HG changeset patch
# User wenzelm
# Date 1158599568 -7200
# Node ID 8b1591393b8d44a5400f74fc7363ae34ce16f04c
# Parent  6b1c69265331214b641d3e20af45b4f2742ad8e0
output: uninterpreted raw symbols -- these are usually LaTeX macros;

diff -r 6b1c69265331 -r 8b1591393b8d src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Mon Sep 18 19:12:47 2006 +0200
+++ b/src/Pure/Thy/html.ML	Mon Sep 18 19:12:48 2006 +0200
@@ -204,10 +204,9 @@
   val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;
 
   fun output_sym 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));
+    (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);