# HG changeset patch
# User wenzelm
# Date 1259953417 -3600
# Node ID cfbf1ff6170d00f8a3300dc362b6c6627c0e75fc
# Parent  1ae222745c4a384dcfad708be62c3eeaa86b6917
output "'" as "'" which is a bit more portable ("'" is defined in XML/XHTML, but not in old-style HTML4);

diff -r 1ae222745c4a -r cfbf1ff6170d src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Fri Dec 04 17:19:59 2009 +0100
+++ b/src/Pure/Thy/html.ML	Fri Dec 04 20:03:37 2009 +0100
@@ -49,7 +49,8 @@
 
 local
   val html_syms = Symtab.make
-   [("\\<spacespace>", (2, "&nbsp;&nbsp;")),
+   [("'", (1, "&#39;")),
+    ("\\<spacespace>", (2, "&nbsp;&nbsp;")),
     ("\\<exclamdown>", (1, "&iexcl;")),
     ("\\<cent>", (1, "&cent;")),
     ("\\<pounds>", (1, "&pound;")),
@@ -197,7 +198,8 @@
   fun output_sym s =
     if Symbol.is_raw s then (1, Symbol.decode_raw s)
     else
-      (case Symtab.lookup html_syms s of SOME x => x
+      (case Symtab.lookup html_syms s of
+        SOME x => x
       | NONE => (size s, XML.text s));
 
   fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);