1.1 --- a/src/Pure/Thy/html.ML	Thu Apr 15 20:30:50 2004 +0200
     1.2 +++ b/src/Pure/Thy/html.ML	Thu Apr 15 20:31:30 2004 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4       | "\\<times>" => (1.0, "&times;")
     1.5       | "\\<emptyset>" => (1.0, "&Oslash;")
     1.6       | "\\<div>" => (1.0, "&divide;")
     1.7 -     | "\\<circ>" => (1.0, "&circ;")    
     1.8 +     | "\\<circ>" => (1.0, "&circ;")
     1.9       | "\\<Alpha>" => (1.0, "&Alpha;")
    1.10       | "\\<Beta>" => (1.0, "&Beta;")
    1.11       | "\\<Gamma>" => (1.0, "&Gamma;")
    1.12 @@ -162,7 +162,7 @@
    1.13       | "\\<propto>" => (1.0, "&prop;")
    1.14       | "\\<infinity>" => (1.0, "&infin;")
    1.15       | "\\<angle>" => (1.0, "&ang;")
    1.16 -     | "\\<and>" => (1.0, "&and;")     
    1.17 +     | "\\<and>" => (1.0, "&and;")
    1.18       | "\\<or>" => (1.0, "&or;")
    1.19       | "\\<inter>" => (1.0, "&cap;")
    1.20       | "\\<union>" => (1.0, "&cup;")
    1.21 @@ -191,11 +191,10 @@
    1.22       | "\\<clubsuit>" => (1.0, "&clubs;")
    1.23       | "\\<heartsuit>" => (1.0, "&hearts;")
    1.24       | "\\<diamondsuit>" => (1.0, "&diams;")
    1.25 -
    1.26       | "\\<lbrakk>" => (2.0, "[|")
    1.27       | "\\<rbrakk>" => (2.0, "|]")
    1.28       | "\\<Longrightarrow>" => (3.0, "==&gt;")
    1.29 -     | "\\<Rightarrow>" => (3.0, "=&gt;")
    1.30 +     | "\\<Rightarrow>" => (2.0, "=&gt;")
    1.31       | "\\<And>" => (2.0, "!!")
    1.32       | "\\<Colon>" => (2.0, "::")
    1.33       | "\\<lparr>" => (2.0, "(|")
    1.34 @@ -203,47 +202,38 @@
    1.35       | "\\<longleftrightarrow>" => (3.0, "&lt;-&gt;")
    1.36       | "\\<longrightarrow>" => (3.0, "--&gt;")
    1.37       | "\\<rightarrow>" => (2.0, "-&gt;")
    1.38 -     | "\\<rightleftharpoons>" => (2.0, "==")
    1.39 -     | "\\<rightharpoonup>" => (2.0, "=&gt;")
    1.40 -     | "\\<leftharpoondown>" => (2.0, "&lt;=")
    1.41 -
    1.42       | "\\<^bsub>" => (0.0, "<sub>")
    1.43       | "\\<^esub>" => (0.0, "</sub>")
    1.44       | "\\<^bsup>" => (0.0, "<sup>")
    1.45       | "\\<^esup>" => (0.0, "</sup>")
    1.46 -(* keep \<^sub> etc, so they are not destroyed by default case *)
    1.47 +     | "\\<^sub>" => (0.0, "\\<^sub>")
    1.48       | "\\<^sup>" => (0.0, "\\<^sup>")
    1.49 -     | "\\<^sub>" => (0.0, "\\<^sub>")
    1.50 +     | "\\<^isub>" => (0.0, "\\<^isub>")
    1.51       | "\\<^isup>" => (0.0, "\\<^isup>")
    1.52 -     | "\\<^isub>" => (0.0, "\\<^isub>")
    1.53       | s => (real (size s), implode (map escape (explode s)));
    1.54  
    1.55    fun add_sym (width, (w: real, s)) = (width + w, s);
    1.56  
    1.57 -  fun script (0, "\\<^sub>") = (1,"<sub>")
    1.58 -    | script (0, "\\<^isub>") = (1,"<sub>")
    1.59 +  fun script (0, "\\<^sub>") = (1, "<sub>")
    1.60 +    | script (0, "\\<^isub>") = (1, "<sub>")
    1.61      | script (1, x) = (0, x ^ "</sub>")
    1.62 -    | script (0, "\\<^sup>") = (2,"<sup>")
    1.63 -    | script (0, "\\<^isup>") = (2,"<sup>")
    1.64 +    | script (0, "\\<^sup>") = (2, "<sup>")
    1.65 +    | script (0, "\\<^isup>") = (2, "<sup>")
    1.66      | script (2, x) = (0, x ^ "</sup>")
    1.67 -    | script (s, x) = (s,x);
    1.68 +    | script (s, x) = (s, x);
    1.69  
    1.70 -  fun scrs (s, []) = (s,[])
    1.71 -    | scrs (s, x::xs) = let val (s', x') = script (s, x)
    1.72 -                            val (s'', xs') = scrs (s', xs)
    1.73 -                        in (s'', x'::xs') end;
    1.74 -                           
    1.75 -  fun scripts ss = #2 (scrs (0,ss));
    1.76 +  fun scripts ss = #2 (foldl_map script (0, ss));
    1.77  in
    1.78  
    1.79  fun output_width str =
    1.80 -  if not (exists_string (equal "<" orf equal ">" orf equal "&") str) then (str, real (size str))
    1.81 +  if not (exists_string (equal "<" orf equal ">" orf equal "&") str)
    1.82 +  then (str, real (size str))
    1.83    else
    1.84      let val (width, syms) = foldl_map add_sym (0.0, map output_sym (Symbol.explode str))
    1.85      in (implode (scripts syms), width) end;
    1.86  
    1.87  val output = #1 o output_width;
    1.88 -val output_symbols = scripts o (map (#2 o output_sym))
    1.89 +val output_symbols = scripts o map (#2 o output_sym);
    1.90  
    1.91  end;
    1.92  
    1.93 @@ -369,9 +359,10 @@
    1.94  
    1.95  (* theory *)
    1.96  
    1.97 -fun verbatim_source ss = "\n</div>\n<hr>\n<div class=\"source\">\n<pre>" ^ 
    1.98 -                         implode (output_symbols ss)  ^ 
    1.99 -                         "</pre>\n</div>\n<hr>\n<div class=\"theorems\">\n";
   1.100 +fun verbatim_source ss =
   1.101 +  "\n</div>\n<hr>\n<div class=\"source\">\n<pre>" ^
   1.102 +  implode (output_symbols ss)  ^
   1.103 +  "</pre>\n</div>\n<hr>\n<div class=\"theorems\">\n";
   1.104  
   1.105  
   1.106  local
   1.107 @@ -400,9 +391,9 @@
   1.108  
   1.109  fun ml_file path str =
   1.110    begin_document ("File " ^ Url.pack path) ^
   1.111 -  "\n</div>\n<hr><div class=\"mlsource\">\n" ^ 
   1.112 -  verbatim str ^ 
   1.113 -  "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^ 
   1.114 +  "\n</div>\n<hr><div class=\"mlsource\">\n" ^
   1.115 +  verbatim str ^
   1.116 +  "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^
   1.117    end_document;
   1.118  
   1.119