src/Pure/Thy/html.ML

      | "\\<threequarters>" => (1.0, "&frac34;")
      | "\\<questiondown>" => (1.0, "&iquest;")
      | "\\<times>" => (1.0, "&times;")
      | "\\<emptyset>" => (1.0, "&Oslash;")
      | "\\<div>" => (1.0, "&divide;")
-     | "\\<circ>" => (1.0, "&circ;")    
+     | "\\<circ>" => (1.0, "&circ;")
      | "\\<Alpha>" => (1.0, "&Alpha;")
      | "\\<Beta>" => (1.0, "&Beta;")
      | "\\<Gamma>" => (1.0, "&Gamma;")
      | "\\<Delta>" => (1.0, "&Delta;")
      | "\\<Epsilon>" => (1.0, "&Epsilon;")

      | "\\<Sum>" => (1.0, "&sum;")
      | "\\<star>" => (1.0, "&lowast;")
      | "\\<propto>" => (1.0, "&prop;")
      | "\\<infinity>" => (1.0, "&infin;")
      | "\\<angle>" => (1.0, "&ang;")
-     | "\\<and>" => (1.0, "&and;")     
+     | "\\<and>" => (1.0, "&and;")
      | "\\<or>" => (1.0, "&or;")
      | "\\<inter>" => (1.0, "&cap;")
      | "\\<union>" => (1.0, "&cup;")
      | "\\<sim>" => (1.0, "&sim;")
      | "\\<cong>" => (1.0, "&cong;")

      | "\\<lozenge>" => (1.0, "&loz;")
      | "\\<spadesuit>" => (1.0, "&spades;")
      | "\\<clubsuit>" => (1.0, "&clubs;")
      | "\\<heartsuit>" => (1.0, "&hearts;")
      | "\\<diamondsuit>" => (1.0, "&diams;")
-
      | "\\<lbrakk>" => (2.0, "[|")
      | "\\<rbrakk>" => (2.0, "|]")
      | "\\<Longrightarrow>" => (3.0, "==&gt;")
-     | "\\<Rightarrow>" => (3.0, "=&gt;")
+     | "\\<Rightarrow>" => (2.0, "=&gt;")
      | "\\<And>" => (2.0, "!!")
      | "\\<Colon>" => (2.0, "::")
      | "\\<lparr>" => (2.0, "(|")
      | "\\<rparr>" => (2.0, "|)")
      | "\\<longleftrightarrow>" => (3.0, "&lt;-&gt;")
      | "\\<longrightarrow>" => (3.0, "--&gt;")
      | "\\<rightarrow>" => (2.0, "-&gt;")
-     | "\\<rightleftharpoons>" => (2.0, "==")
-     | "\\<rightharpoonup>" => (2.0, "=&gt;")
-     | "\\<leftharpoondown>" => (2.0, "&lt;=")
-
      | "\\<^bsub>" => (0.0, "<sub>")
      | "\\<^esub>" => (0.0, "</sub>")
      | "\\<^bsup>" => (0.0, "<sup>")
      | "\\<^esup>" => (0.0, "</sup>")
-(* keep \<^sub> etc, so they are not destroyed by default case *)
+     | "\\<^sub>" => (0.0, "\\<^sub>")
      | "\\<^sup>" => (0.0, "\\<^sup>")
-     | "\\<^sub>" => (0.0, "\\<^sub>")
+     | "\\<^isub>" => (0.0, "\\<^isub>")
      | "\\<^isup>" => (0.0, "\\<^isup>")
-     | "\\<^isub>" => (0.0, "\\<^isub>")
      | s => (real (size s), implode (map escape (explode s)));
 
   fun add_sym (width, (w: real, s)) = (width + w, s);
 
-  fun script (0, "\\<^sub>") = (1,"<sub>")
-    | script (0, "\\<^isub>") = (1,"<sub>")
+  fun script (0, "\\<^sub>") = (1, "<sub>")
+    | script (0, "\\<^isub>") = (1, "<sub>")
     | script (1, x) = (0, x ^ "</sub>")
-    | script (0, "\\<^sup>") = (2,"<sup>")
-    | script (0, "\\<^isup>") = (2,"<sup>")
+    | script (0, "\\<^sup>") = (2, "<sup>")
+    | script (0, "\\<^isup>") = (2, "<sup>")
     | script (2, x) = (0, x ^ "</sup>")
-    | script (s, x) = (s,x);
-
-  fun scrs (s, []) = (s,[])
-    | scrs (s, x::xs) = let val (s', x') = script (s, x)
-                            val (s'', xs') = scrs (s', xs)
-                        in (s'', x'::xs') end;
-                           
-  fun scripts ss = #2 (scrs (0,ss));
+    | script (s, x) = (s, x);
+
+  fun scripts ss = #2 (foldl_map script (0, ss));
 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 "&") str)
+  then (str, real (size str))
   else
     let val (width, syms) = foldl_map add_sym (0.0, map output_sym (Symbol.explode str))
     in (implode (scripts syms), width) end;
 
 val output = #1 o output_width;
-val output_symbols = scripts o (map (#2 o output_sym))
+val output_symbols = scripts o map (#2 o output_sym);
 
 end;
 
 
 val _ = Symbol.add_mode htmlN (output_width, Symbol.default_indent);

       "</ul>\n</div>\n<hr>\n<div class=\"sessions\">\n<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
 
 
 (* theory *)
 
-fun verbatim_source ss = "\n</div>\n<hr>\n<div class=\"source\">\n<pre>" ^ 
-                         implode (output_symbols ss)  ^ 
-                         "</pre>\n</div>\n<hr>\n<div class=\"theorems\">\n";
+fun verbatim_source ss =
+  "\n</div>\n<hr>\n<div class=\"source\">\n<pre>" ^
+  implode (output_symbols ss)  ^
+  "</pre>\n</div>\n<hr>\n<div class=\"theorems\">\n";
 
 
 local
   fun encl None = enclose "[" "]"
     | encl (Some false) = enclose "(" ")"

 
 (* ML file *)
 
 fun ml_file path str =
   begin_document ("File " ^ Url.pack path) ^
-  "\n</div>\n<hr><div class=\"mlsource\">\n" ^ 
-  verbatim str ^ 
-  "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^ 
+  "\n</div>\n<hr><div class=\"mlsource\">\n" ^
+  verbatim str ^
+  "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^
   end_document;
 
 
 (* theorems *)