# HG changeset patch
# User wenzelm
# Date 968969871 -7200
# Node ID 6342d9c7fe46b9b8d5d98ffac16bee1fe0b5f0a6
# Parent  765208b5dd236379c9a0921d9c71361a5096975a
handle more symbols;

diff -r 765208b5dd23 -r 6342d9c7fe46 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Fri Sep 15 00:17:11 2000 +0200
+++ b/src/Pure/Thy/html.ML	Fri Sep 15 00:17:51 2000 +0200
@@ -63,12 +63,37 @@
   val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;
 
   val output_sym =
-    fn "\\<not>" => (1.0, "&not;")
+    fn "\\<spacespace>" => (2.0, "&nbsp;&nbsp;")
+     | "\\<exclamdown>" => (1.0, "&iexcl;")
+     | "\\<cent>" => (1.0, "&cent;")
+     | "\\<pounds>" => (1.0, "&pound;")
+     | "\\<currency>" => (1.0, "&curren;")
+     | "\\<yen>" => (1.0, "&yen;")
+     | "\\<bar>" => (1.0, "&brvbar;")
+     | "\\<section>" => (1.0, "&sect;")
+     | "\\<copyright>" => (1.0, "&copy;")
+     | "\\<ordfeminine>" => (1.0, "&ordf;")
+     | "\\<guillemotleft>" => (1.0, "&laquo;")
+     | "\\<not>" => (1.0, "&not;")
      | "\\<hyphen>" => (1.0, "&shy;")
+     | "\\<registered>" => (1.0, "&reg;")
+     | "\\<macron>" => (1.0, "&macr;")
+     | "\\<degree>" => (1.0, "&deg;")
+     | "\\<plusminus>" => (1.0, "&plusmn;")
+     | "\\<twosuperior>" => (1.0, "&sup2;")
+     | "\\<threesuperior>" => (1.0, "&sup3;")
+     | "\\<mu>" => (1.0, "&micro;")
+     | "\\<paragraph>" => (1.0, "&para;")
      | "\\<cdot>" => (1.0, "&middot;")
+     | "\\<onesuperior>" => (1.0, "&sup1;")
+     | "\\<ordmasculine>" => (1.0, "&ordm;")
+     | "\\<guillemotright>" => (1.0, "&raquo;")
+     | "\\<onequarter>" => (1.0, "&frac14;")
+     | "\\<onehalf>" => (1.0, "&frac12;")
+     | "\\<threequarters>" => (1.0, "&frac34;")
+     | "\\<questiondown>" => (1.0, "&iquest;")
      | "\\<times>" => (1.0, "&times;")
-     | "\\<copyright>" => (1.0, "&copy;")
-     | "\\<mu>" => (1.0, "&micro;")
+     | "\\<div>" => (1.0, "&divide;")
      | s => (real (size s), implode (map escape (explode s)));
 
   fun add_sym (width, (w: real, s)) = (width + w, s);