convert symbols to HTML 4.0 character entities,
authorkleing
Tue Apr 13 10:45:35 2004 +0200 (2004-04-13)
changeset 14552e88f52b775a5
parent 14551 2cb6ff394bfb
child 14553 4740fc2da7bb
convert symbols to HTML 4.0 character entities,
convert some common remaining symbols to ASCII (e.g. lbrakk -> [|)
src/Pure/Thy/html.ML
     1.1 --- a/src/Pure/Thy/html.ML	Tue Apr 13 09:42:40 2004 +0200
     1.2 +++ b/src/Pure/Thy/html.ML	Tue Apr 13 10:45:35 2004 +0200
     1.3 @@ -95,11 +95,121 @@
     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 +     | "\\<Alpha>" => (1.0, "&Alpha;")
     1.9 +     | "\\<Beta>" => (1.0, "&Beta;")
    1.10 +     | "\\<Gamma>" => (1.0, "&Gamma;")
    1.11 +     | "\\<Delta>" => (1.0, "&Delta;")
    1.12 +     | "\\<Epsilon>" => (1.0, "&Epsilon;")
    1.13 +     | "\\<Zeta>" => (1.0, "&Zeta;")
    1.14 +     | "\\<Eta>" => (1.0, "&Eta;")
    1.15 +     | "\\<Theta>" => (1.0, "&Theta;")
    1.16 +     | "\\<Iota>" => (1.0, "&Iota;")
    1.17 +     | "\\<Kappa>" => (1.0, "&Kappa;")
    1.18 +     | "\\<Lambda>" => (1.0, "&Lambda;")
    1.19 +     | "\\<Mu>" => (1.0, "&Mu;")
    1.20 +     | "\\<Nu>" => (1.0, "&Nu;")
    1.21 +     | "\\<Xi>" => (1.0, "&Xi;")
    1.22 +     | "\\<Omicron>" => (1.0, "&Omicron;")
    1.23 +     | "\\<Pi>" => (1.0, "&Pi;")
    1.24 +     | "\\<Rho>" => (1.0, "&Rho;")
    1.25 +     | "\\<Sigma>" => (1.0, "&Sigma;")
    1.26 +     | "\\<Tau>" => (1.0, "&Tau;")
    1.27 +     | "\\<Upsilon>" => (1.0, "&Upsilon;")
    1.28 +     | "\\<Phi>" => (1.0, "&Phi;")
    1.29 +     | "\\<Chi>" => (1.0, "&Chi;")
    1.30 +     | "\\<Psi>" => (1.0, "&Psi;")
    1.31 +     | "\\<Omega>" => (1.0, "&Omega;")
    1.32 +     | "\\<alpha>" => (1.0, "&alpha;")
    1.33 +     | "\\<beta>" => (1.0, "&beta;")
    1.34 +     | "\\<gamma>" => (1.0, "&gamma;")
    1.35 +     | "\\<delta>" => (1.0, "&delta;")
    1.36 +     | "\\<epsilon>" => (1.0, "&epsilon;")
    1.37 +     | "\\<zeta>" => (1.0, "&zeta;")
    1.38 +     | "\\<eta>" => (1.0, "&eta;")
    1.39 +     | "\\<theta>" => (1.0, "&thetasym;")
    1.40 +     | "\\<iota>" => (1.0, "&iota;")
    1.41 +     | "\\<kappa>" => (1.0, "&kappa;")
    1.42 +     | "\\<lambda>" => (1.0, "&lambda;")
    1.43 +     | "\\<mu>" => (1.0, "&mu;")
    1.44 +     | "\\<nu>" => (1.0, "&nu;")
    1.45 +     | "\\<xi>" => (1.0, "&xi;")
    1.46 +     | "\\<omicron>" => (1.0, "&omicron;")
    1.47 +     | "\\<pi>" => (1.0, "&pi;")
    1.48 +     | "\\<rho>" => (1.0, "&rho;")
    1.49 +     | "\\<sigma>" => (1.0, "&sigma;")
    1.50 +     | "\\<tau>" => (1.0, "&tau;")
    1.51 +     | "\\<upsilon>" => (1.0, "&upsilon;")
    1.52 +     | "\\<phi>" => (1.0, "&phi;")
    1.53 +     | "\\<chi>" => (1.0, "&chi;")
    1.54 +     | "\\<psi>" => (1.0, "&psi;")
    1.55 +     | "\\<omega>" => (1.0, "&omega;")
    1.56 +     | "\\<buller>" => (1.0, "&bull;")
    1.57 +     | "\\<dots>" => (1.0, "&hellip;")
    1.58 +     | "\\<Re>" => (1.0, "&real;")
    1.59 +     | "\\<Im>" => (1.0, "&image;")
    1.60 +     | "\\<wp>" => (1.0, "&weierp;")
    1.61 +     | "\\<forall>" => (1.0, "&forall;")
    1.62 +     | "\\<partial>" => (1.0, "&part;")
    1.63 +     | "\\<exists>" => (1.0, "&exist;")
    1.64 +     | "\\<emptyset>" => (1.0, "&empty;")
    1.65 +     | "\\<nabla>" => (1.0, "&nabla;")
    1.66 +     | "\\<in>" => (1.0, "&isin;")
    1.67 +     | "\\<notin>" => (1.0, "&notin;")
    1.68 +     | "\\<star>" => (1.0, "&lowast;")
    1.69 +     | "\\<propto>" => (1.0, "&prop;")
    1.70 +     | "\\<infinity>" => (1.0, "&infin;")
    1.71 +     | "\\<angle>" => (1.0, "&ang;")
    1.72 +     | "\\<and>" => (1.0, "&and;")     
    1.73 +     | "\\<or>" => (1.0, "&or;")
    1.74 +     | "\\<inter>" => (1.0, "&cap;")
    1.75 +     | "\\<union>" => (1.0, "&cup;")
    1.76 +     | "\\<sim>" => (1.0, "&sim;")
    1.77 +     | "\\<cong>" => (1.0, "&cong;")
    1.78 +     | "\\<approx>" => (1.0, "&asymp;")
    1.79 +     | "\\<noteq>" => (1.0, "&ne;")
    1.80 +     | "\\<equiv>" => (1.0, "&equiv;")
    1.81 +     | "\\<le>" => (1.0, "&le;")
    1.82 +     | "\\<ge>" => (1.0, "&ge;")
    1.83 +     | "\\<subset>" => (1.0, "&sub;")
    1.84 +     | "\\<supset>" => (1.0, "&sup;")
    1.85 +     | "\\<subseteq>" => (1.0, "&sube;")
    1.86 +     | "\\<supseteq>" => (1.0, "&supe;")
    1.87 +     | "\\<oplus>" => (1.0, "&oplus;")
    1.88 +     | "\\<otimes>" => (1.0, "&otimes;")
    1.89 +     | "\\<bottom>" => (1.0, "&perp;")
    1.90 +     | "\\<lceil>" => (1.0, "&lceil;")
    1.91 +     | "\\<rceil>" => (1.0, "&rceil;")
    1.92 +     | "\\<lfloor>" => (1.0, "&lfloor;")
    1.93 +     | "\\<rfloor>" => (1.0, "&rfloor;")
    1.94 +     | "\\<langle>" => (1.0, "&lang;")
    1.95 +     | "\\<rangle>" => (1.0, "&rang;")
    1.96 +     | "\\<lozenge>" => (1.0, "&loz;")
    1.97 +     | "\\<spadesuit>" => (1.0, "&spades;")
    1.98 +     | "\\<clubsuit>" => (1.0, "&clubs;")
    1.99 +     | "\\<heartsuit>" => (1.0, "&hearts;")
   1.100 +     | "\\<diamondsuit>" => (1.0, "&diams;")
   1.101 +
   1.102 +     | "\\<lbrakk>" => (2.0, "[|")
   1.103 +     | "\\<rbrakk>" => (2.0, "|]")
   1.104 +     | "\\<Longrightarrow>" => (3.0, "==&gt;")
   1.105 +     | "\\<Rightarrow>" => (3.0, "=&gt;")
   1.106 +     | "\\<And>" => (2.0, "!!")
   1.107 +     | "\\<Colon>" => (2.0, "::")
   1.108 +     | "\\<lparr>" => (2.0, "(|")
   1.109 +     | "\\<rparr>" => (2.0, "|)")
   1.110 +     | "\\<longleftrightarrow>" => (3.0, "&lt;-&gt;")
   1.111 +     | "\\<longrightarrow>" => (3.0, "--&gt;")
   1.112 +     | "\\<rightarrow>" => (2.0, "-&gt;")
   1.113 +     | "\\<rightleftharpoons>" => (2.0, "==")
   1.114 +     | "\\<rightharpoonup>" => (2.0, "=&gt;")
   1.115 +     | "\\<leftharpoondown>" => (2.0, "&lt;=")
   1.116 +
   1.117       | "\\<^bsub>" => (0.0, "<sub>")
   1.118       | "\\<^esub>" => (0.0, "</sub>")
   1.119       | "\\<^bsup>" => (0.0, "<sup>")
   1.120       | "\\<^esup>" => (0.0, "</sup>")
   1.121 -(* keep \<^sub> etc, so it does not get destroyed by default case *)
   1.122 +(* keep \<^sub> etc, so they are not destroyed by default case *)
   1.123       | "\\<^sup>" => (0.0, "\\<^sup>")
   1.124       | "\\<^sub>" => (0.0, "\\<^sub>")
   1.125       | "\\<^isup>" => (0.0, "\\<^isup>")