1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/WWW_Find/www/find_theorems.js	Fri Nov 20 18:36:44 2009 +1100
     1.3 @@ -0,0 +1,410 @@
     1.4 +/* $Id$
     1.5 + * Author: Timothy Bourke, NICTA
     1.6 + */
     1.7 +var utf8 = new Object();
     1.8 +utf8['\\<supseteq>'] = '⊇';
     1.9 +utf8['\\<KK>'] = '𝔎';
    1.10 +utf8['\\<up>'] = '↑';
    1.11 +utf8['\\<otimes>'] = '⊗';
    1.12 +utf8['\\<aa>'] = '𝔞';
    1.13 +utf8['\\<dagger>'] = '†';
    1.14 +utf8['\\<frown>'] = '⌢';
    1.15 +utf8['\\<guillemotleft>'] = '«';
    1.16 +utf8['\\<qq>'] = '𝔮';
    1.17 +utf8['\\<X>'] = '𝒳';
    1.18 +utf8['\\<triangleright>'] = '▹';
    1.19 +utf8['\\<guillemotright>'] = '»';
    1.20 +utf8['\\<nu>'] = 'ν';
    1.21 +utf8['\\<sim>'] = '∼';
    1.22 +utf8['\\<rightharpoondown>'] = '⇁';
    1.23 +utf8['\\<p>'] = '𝗉';
    1.24 +utf8['\\<Up>'] = '⇑';
    1.25 +utf8['\\<triangleq>'] = '≜';
    1.26 +utf8['\\<nine>'] = '𝟵';
    1.27 +utf8['\\<preceq>'] = '≼';
    1.28 +utf8['\\<nabla>'] = '∇';
    1.29 +utf8['\\<FF>'] = '𝔉';
    1.30 +utf8['\\<Im>'] = 'ℑ';
    1.31 +utf8['\\<VV>'] = '𝔙';
    1.32 +utf8['\\<spacespace>'] = '␣';
    1.33 +utf8['\\<and>'] = '∧';
    1.34 +utf8['\\<mapsto>'] = '↦';
    1.35 +utf8['\\<ll>'] = '𝔩';
    1.36 +utf8['\\<F>'] = 'ℱ';
    1.37 +utf8['\\<degree>'] = '°';
    1.38 +utf8['\\<beta>'] = 'β';
    1.39 +utf8['\\<Colon>'] = '∷';
    1.40 +utf8['\\<bool>'] = '𝔹';
    1.41 +utf8['\\<e>'] = '𝖾';
    1.42 +utf8['\\<lozenge>'] = '◊';
    1.43 +utf8['\\<u>'] = '𝗎';
    1.44 +utf8['\\<sharp>'] = '♯';
    1.45 +utf8['\\<Longleftrightarrow>'] = '⟺';
    1.46 +utf8['\\<Otimes>'] = '⨂';
    1.47 +utf8['\\<EE>'] = '𝔈';
    1.48 +utf8['\\<I>'] = 'ℐ';
    1.49 +utf8['\\<UU>'] = '𝔘';
    1.50 +utf8['\\<exclamdown>'] = '¡';
    1.51 +utf8['\\<dots>'] = '…';
    1.52 +utf8['\\<N>'] = '𝒩';
    1.53 +utf8['\\<kk>'] = '𝔨';
    1.54 +utf8['\\<plusminus>'] = '±';
    1.55 +utf8['\\<E>'] = 'ℰ';
    1.56 +utf8['\\<triangle>'] = '△';
    1.57 +utf8['\\<eta>'] = 'η';
    1.58 +utf8['\\<triangleleft>'] = '◃';
    1.59 +utf8['\\<chi>'] = 'χ';
    1.60 +utf8['\\<z>'] = '𝗓';
    1.61 +utf8['\\<hungarumlaut>'] = '˝';
    1.62 +utf8['\\<partial>'] = '∂';
    1.63 +utf8['\\<three>'] = '𝟯';
    1.64 +utf8['\\<lesssim>'] = '≲';
    1.65 +utf8['\\<subset>'] = '⊂';
    1.66 +utf8['\\<H>'] = 'ℋ';
    1.67 +utf8['\\<leftarrow>'] = '←';
    1.68 +utf8['\\<PP>'] = '𝔓';
    1.69 +utf8['\\<sqsupseteq>'] = '⊒';
    1.70 +utf8['\\<R>'] = 'ℛ';
    1.71 +utf8['\\<bowtie>'] = '⨝';
    1.72 +utf8['\\<C>'] = '𝒞';
    1.73 +utf8['\\<ddagger>'] = '‡';
    1.74 +utf8['\\<ff>'] = '𝔣';
    1.75 +utf8['\\<turnstile>'] = '⊢';
    1.76 +utf8['\\<bar>'] = '¦';
    1.77 +utf8['\\<propto>'] = '∝';
    1.78 +utf8['\\<S>'] = '𝒮';
    1.79 +utf8['\\<vv>'] = '𝔳';
    1.80 +utf8['\\<lhd>'] = '⊲';
    1.81 +utf8['\\<paragraph>'] = '¶';
    1.82 +utf8['\\<mu>'] = 'μ';
    1.83 +utf8['\\<rightharpoonup>'] = '⇀';
    1.84 +utf8['\\<Inter>'] = '⋂';
    1.85 +utf8['\\<o>'] = '𝗈';
    1.86 +utf8['\\<asymp>'] = '≍';
    1.87 +utf8['\\<Leftarrow>'] = '⇐';
    1.88 +utf8['\\<Sqinter>'] = '⨅';
    1.89 +utf8['\\<eight>'] = '𝟴';
    1.90 +utf8['\\<succeq>'] = '≽';
    1.91 +utf8['\\<forall>'] = '∀';
    1.92 +utf8['\\<complex>'] = 'ℂ';
    1.93 +utf8['\\<GG>'] = '𝔊';
    1.94 +utf8['\\<Coprod>'] = '∐';
    1.95 +utf8['\\<L>'] = 'ℒ';
    1.96 +utf8['\\<WW>'] = '𝔚';
    1.97 +utf8['\\<leadsto>'] = '↝';
    1.98 +utf8['\\<D>'] = '𝒟';
    1.99 +utf8['\\<angle>'] = '∠';
   1.100 +utf8['\\<section>'] = '§';
   1.101 +utf8['\\<TTurnstile>'] = '⊫';
   1.102 +utf8['\\<mm>'] = '𝔪';
   1.103 +utf8['\\<T>'] = '𝒯';
   1.104 +utf8['\\<alpha>'] = 'α';
   1.105 +utf8['\\<leftharpoondown>'] = '↽';
   1.106 +utf8['\\<rho>'] = 'ρ';
   1.107 +utf8['\\<wrong>'] = '≀';
   1.108 +utf8['\\<l>'] = '𝗅';
   1.109 +utf8['\\<doteq>'] = '≐';
   1.110 +utf8['\\<times>'] = '×';
   1.111 +utf8['\\<noteq>'] = '≠';
   1.112 +utf8['\\<rangle>'] = '⟩';
   1.113 +utf8['\\<div>'] = '÷';
   1.114 +utf8['\\<Longrightarrow>'] = '⟹';
   1.115 +utf8['\\<BB>'] = '𝔅';
   1.116 +utf8['\\<sqsupset>'] = '⊐';
   1.117 +utf8['\\<rightarrow>'] = '→';
   1.118 +utf8['\\<real>'] = 'ℝ';
   1.119 +utf8['\\<hh>'] = '𝔥';
   1.120 +utf8['\\<Phi>'] = 'Φ';
   1.121 +utf8['\\<integral>'] = '∫';
   1.122 +utf8['\\<CC>'] = 'ℭ';
   1.123 +utf8['\\<euro>'] = '€';
   1.124 +utf8['\\<xx>'] = '𝔵';
   1.125 +utf8['\\<Y>'] = '𝒴';
   1.126 +utf8['\\<zeta>'] = 'ζ';
   1.127 +utf8['\\<longleftarrow>'] = '⟵';
   1.128 +utf8['\\<a>'] = '𝖺';
   1.129 +utf8['\\<onequarter>'] = '¼';
   1.130 +utf8['\\<And>'] = '⋀';
   1.131 +utf8['\\<downharpoonright>'] = '⇂';
   1.132 +utf8['\\<phi>'] = 'φ';
   1.133 +utf8['\\<q>'] = '𝗊';
   1.134 +utf8['\\<Rightarrow>'] = '⇒';
   1.135 +utf8['\\<clubsuit>'] = '♣';
   1.136 +utf8['\\<ggreater>'] = '≫';
   1.137 +utf8['\\<two>'] = '𝟮';
   1.138 +utf8['\\<succ>'] = '≻';
   1.139 +utf8['\\<AA>'] = '𝔄';
   1.140 +utf8['\\<lparr>'] = '⦇';
   1.141 +utf8['\\<Squnion>'] = '⨆';
   1.142 +utf8['\\<HH>'] = 'ℌ';
   1.143 +utf8['\\<sqsubseteq>'] = '⊑';
   1.144 +utf8['\\<QQ>'] = '𝔔';
   1.145 +utf8['\\<setminus>'] = '∖';
   1.146 +utf8['\\<Lambda>'] = 'Λ';
   1.147 +utf8['\\<Re>'] = 'ℜ';
   1.148 +utf8['\\<J>'] = '𝒥';
   1.149 +utf8['\\<gg>'] = '𝔤';
   1.150 +utf8['\\<hyphen>'] = '­';
   1.151 +utf8['\\<B>'] = 'ℬ';
   1.152 +utf8['\\<Z>'] = '𝒵';
   1.153 +utf8['\\<ww>'] = '𝔴';
   1.154 +utf8['\\<lambda>'] = 'λ';
   1.155 +utf8['\\<onehalf>'] = '½';
   1.156 +utf8['\\<f>'] = '𝖿';
   1.157 +utf8['\\<Or>'] = '⋁';
   1.158 +utf8['\\<v>'] = '𝗏';
   1.159 +utf8['\\<natural>'] = '♮';
   1.160 +utf8['\\<seven>'] = '𝟳';
   1.161 +utf8['\\<Oplus>'] = '⨁';
   1.162 +utf8['\\<subseteq>'] = '⊆';
   1.163 +utf8['\\<rfloor>'] = '⌋';
   1.164 +utf8['\\<LL>'] = '𝔏';
   1.165 +utf8['\\<Sum>'] = '∑';
   1.166 +utf8['\\<ominus>'] = '⊖';
   1.167 +utf8['\\<bb>'] = '𝔟';
   1.168 +utf8['\\<Pi>'] = 'Π';
   1.169 +utf8['\\<cent>'] = '¢';
   1.170 +utf8['\\<diamond>'] = '◇';
   1.171 +utf8['\\<mho>'] = '℧';
   1.172 +utf8['\\<O>'] = '𝒪';
   1.173 +utf8['\\<rr>'] = '𝔯';
   1.174 +utf8['\\<twosuperior>'] = '²';
   1.175 +utf8['\\<leftharpoonup>'] = '↼';
   1.176 +utf8['\\<pi>'] = 'π';
   1.177 +utf8['\\<k>'] = '𝗄';
   1.178 +utf8['\\<star>'] = '⋆';
   1.179 +utf8['\\<rightleftharpoons>'] = '⇌';
   1.180 +utf8['\\<equiv>'] = '≡';
   1.181 +utf8['\\<langle>'] = '⟨';
   1.182 +utf8['\\<Longleftarrow>'] = '⟸';
   1.183 +utf8['\\<nexists>'] = '∄';
   1.184 +utf8['\\<Odot>'] = '⨀';
   1.185 +utf8['\\<lfloor>'] = '⌊';
   1.186 +utf8['\\<sqsubset>'] = '⊏';
   1.187 +utf8['\\<SS>'] = '𝔖';
   1.188 +utf8['\\<box>'] = '□';
   1.189 +utf8['\\<index>'] = 'ı';
   1.190 +utf8['\\<pounds>'] = '£';
   1.191 +utf8['\\<Upsilon>'] = 'Υ';
   1.192 +utf8['\\<ii>'] = '𝔦';
   1.193 +utf8['\\<hookleftarrow>'] = '↩';
   1.194 +utf8['\\<P>'] = '𝒫';
   1.195 +utf8['\\<threesuperior>'] = '³';
   1.196 +utf8['\\<epsilon>'] = 'ε';
   1.197 +utf8['\\<yy>'] = '𝔶';
   1.198 +utf8['\\<h>'] = '𝗁';
   1.199 +utf8['\\<upsilon>'] = 'υ';
   1.200 +utf8['\\<x>'] = '𝗑';
   1.201 +utf8['\\<not>'] = '¬';
   1.202 +utf8['\\<le>'] = '≤';
   1.203 +utf8['\\<one>'] = '𝟭';
   1.204 +utf8['\\<cdots>'] = '⋯';
   1.205 +utf8['\\<some>'] = 'ϵ';
   1.206 +utf8['\\<Prod>'] = '∏';
   1.207 +utf8['\\<NN>'] = '𝔑';
   1.208 +utf8['\\<squnion>'] = '⊔';
   1.209 +utf8['\\<dd>'] = '𝔡';
   1.210 +utf8['\\<top>'] = '⊤';
   1.211 +utf8['\\<dieresis>'] = '¨';
   1.212 +utf8['\\<tt>'] = '𝔱';
   1.213 +utf8['\\<U>'] = '𝒰';
   1.214 +utf8['\\<unlhd>'] = '⊴';
   1.215 +utf8['\\<cedilla>'] = '¸';
   1.216 +utf8['\\<kappa>'] = 'κ';
   1.217 +utf8['\\<amalg>'] = '⨿';
   1.218 +utf8['\\<restriction>'] = '↾';
   1.219 +utf8['\\<struct>'] = '⋄';
   1.220 +utf8['\\<m>'] = '𝗆';
   1.221 +utf8['\\<six>'] = '𝟲';
   1.222 +utf8['\\<midarrow>'] = '─';
   1.223 +utf8['\\<lbrace>'] = '⦃';
   1.224 +utf8['\\<lessapprox>'] = '⪅';
   1.225 +utf8['\\<MM>'] = '𝔐';
   1.226 +utf8['\\<down>'] = '↓';
   1.227 +utf8['\\<oplus>'] = '⊕';
   1.228 +utf8['\\<wp>'] = '℘';
   1.229 +utf8['\\<surd>'] = '√';
   1.230 +utf8['\\<cc>'] = '𝔠';
   1.231 +utf8['\\<bottom>'] = '⊥';
   1.232 +utf8['\\<copyright>'] = '©';
   1.233 +utf8['\\<ZZ>'] = 'ℨ';
   1.234 +utf8['\\<union>'] = '∪';
   1.235 +utf8['\\<V>'] = '𝒱';
   1.236 +utf8['\\<ss>'] = '𝔰';
   1.237 +utf8['\\<unrhd>'] = '⊵';
   1.238 +utf8['\\<onesuperior>'] = '¹';
   1.239 +utf8['\\<b>'] = '𝖻';
   1.240 +utf8['\\<downharpoonleft>'] = '⇃';
   1.241 +utf8['\\<cdot>'] = '⋅';
   1.242 +utf8['\\<r>'] = '𝗋';
   1.243 +utf8['\\<Midarrow>'] = '═';
   1.244 +utf8['\\<Down>'] = '⇓';
   1.245 +utf8['\\<diamondsuit>'] = '♢';
   1.246 +utf8['\\<rbrakk>'] = '⟧';
   1.247 +utf8['\\<lless>'] = '≪';
   1.248 +utf8['\\<longleftrightarrow>'] = '⟷';
   1.249 +utf8['\\<prec>'] = '≺';
   1.250 +utf8['\\<emptyset>'] = '∅';
   1.251 +utf8['\\<rparr>'] = '⦈';
   1.252 +utf8['\\<Delta>'] = 'Δ';
   1.253 +utf8['\\<XX>'] = '𝔛';
   1.254 +utf8['\\<parallel>'] = '∥';
   1.255 +utf8['\\<K>'] = '𝒦';
   1.256 +utf8['\\<nn>'] = '𝔫';
   1.257 +utf8['\\<registered>'] = '®';
   1.258 +utf8['\\<M>'] = 'ℳ';
   1.259 +utf8['\\<delta>'] = 'δ';
   1.260 +utf8['\\<threequarters>'] = '¾';
   1.261 +utf8['\\<g>'] = '𝗀';
   1.262 +utf8['\\<cong>'] = '≅';
   1.263 +utf8['\\<tau>'] = 'τ';
   1.264 +utf8['\\<w>'] = '𝗐';
   1.265 +utf8['\\<ge>'] = '≥';
   1.266 +utf8['\\<flat>'] = '♭';
   1.267 +utf8['\\<zero>'] = '𝟬';
   1.268 +utf8['\\<Uplus>'] = '⨄';
   1.269 +utf8['\\<longmapsto>'] = '⟼';
   1.270 +utf8['\\<supset>'] = '⊃';
   1.271 +utf8['\\<in>'] = '∈';
   1.272 +utf8['\\<sqinter>'] = '⊓';
   1.273 +utf8['\\<OO>'] = '𝔒';
   1.274 +utf8['\\<updown>'] = '↕';
   1.275 +utf8['\\<circ>'] = '∘';
   1.276 +utf8['\\<rat>'] = 'ℚ';
   1.277 +utf8['\\<stileturn>'] = '⊣';
   1.278 +utf8['\\<ee>'] = '𝔢';
   1.279 +utf8['\\<Omega>'] = 'Ω';
   1.280 +utf8['\\<or>'] = '∨';
   1.281 +utf8['\\<inverse>'] = '¯';
   1.282 +utf8['\\<rhd>'] = '⊳';
   1.283 +utf8['\\<uu>'] = '𝔲';
   1.284 +utf8['\\<iota>'] = 'ι';
   1.285 +utf8['\\<d>'] = '𝖽';
   1.286 +utf8['\\<questiondown>'] = '¿';
   1.287 +utf8['\\<Union>'] = '⋃';
   1.288 +utf8['\\<omega>'] = 'ω';
   1.289 +utf8['\\<approx>'] = '≈';
   1.290 +utf8['\\<t>'] = '𝗍';
   1.291 +utf8['\\<Updown>'] = '⇕';
   1.292 +utf8['\\<spadesuit>'] = '♠';
   1.293 +utf8['\\<five>'] = '𝟱';
   1.294 +utf8['\\<exists>'] = '∃';
   1.295 +utf8['\\<rceil>'] = '⌉';
   1.296 +utf8['\\<JJ>'] = '𝔍';
   1.297 +utf8['\\<minusplus>'] = '∓';
   1.298 +utf8['\\<nat>'] = 'ℕ';
   1.299 +utf8['\\<oslash>'] = '⊘';
   1.300 +utf8['\\<A>'] = '𝒜';
   1.301 +utf8['\\<Xi>'] = 'Ξ';
   1.302 +utf8['\\<currency>'] = '¤';
   1.303 +utf8['\\<Turnstile>'] = '⊨';
   1.304 +utf8['\\<hookrightarrow>'] = '↪';
   1.305 +utf8['\\<pp>'] = '𝔭';
   1.306 +utf8['\\<Q>'] = '𝒬';
   1.307 +utf8['\\<aleph>'] = 'ℵ';
   1.308 +utf8['\\<acute>'] = '´';
   1.309 +utf8['\\<xi>'] = 'ξ';
   1.310 +utf8['\\<simeq>'] = '≃';
   1.311 +utf8['\\<i>'] = '𝗂';
   1.312 +utf8['\\<Join>'] = '⋈';
   1.313 +utf8['\\<y>'] = '𝗒';
   1.314 +utf8['\\<lbrakk>'] = '⟦';
   1.315 +utf8['\\<greatersim>'] = '≳';
   1.316 +utf8['\\<greaterapprox>'] = '⪆';
   1.317 +utf8['\\<longrightarrow>'] = '⟶';
   1.318 +utf8['\\<lceil>'] = '⌈';
   1.319 +utf8['\\<Gamma>'] = 'Γ';
   1.320 +utf8['\\<odot>'] = '⊙';
   1.321 +utf8['\\<YY>'] = '𝔜';
   1.322 +utf8['\\<infinity>'] = '∞';
   1.323 +utf8['\\<Sigma>'] = 'Σ';
   1.324 +utf8['\\<yen>'] = '¥';
   1.325 +utf8['\\<int>'] = 'ℤ';
   1.326 +utf8['\\<tturnstile>'] = '⊩';
   1.327 +utf8['\\<oo>'] = '𝔬';
   1.328 +utf8['\\<ointegral>'] = '∮';
   1.329 +utf8['\\<gamma>'] = 'γ';
   1.330 +utf8['\\<upharpoonleft>'] = '↿';
   1.331 +utf8['\\<sigma>'] = 'σ';
   1.332 +utf8['\\<n>'] = '𝗇';
   1.333 +utf8['\\<rbrace>'] = '⦄';
   1.334 +utf8['\\<DD>'] = '𝔇';
   1.335 +utf8['\\<notin>'] = '∉';
   1.336 +utf8['\\<j>'] = '𝗃';
   1.337 +utf8['\\<uplus>'] = '⊎';
   1.338 +utf8['\\<leftrightarrow>'] = '↔';
   1.339 +utf8['\\<TT>'] = '𝔗';
   1.340 +utf8['\\<bullet>'] = '∙';
   1.341 +utf8['\\<Theta>'] = 'Θ';
   1.342 +utf8['\\<smile>'] = '⌣';
   1.343 +utf8['\\<G>'] = '𝒢';
   1.344 +utf8['\\<jj>'] = '𝔧';
   1.345 +utf8['\\<inter>'] = '∩';
   1.346 +utf8['\\<Psi>'] = 'Ψ';
   1.347 +utf8['\\<ordfeminine>'] = 'ª';
   1.348 +utf8['\\<W>'] = '𝒲';
   1.349 +utf8['\\<zz>'] = '𝔷';
   1.350 +utf8['\\<theta>'] = 'θ';
   1.351 +utf8['\\<ordmasculine>'] = 'º';
   1.352 +utf8['\\<c>'] = '𝖼';
   1.353 +utf8['\\<psi>'] = 'ψ';
   1.354 +utf8['\\<s>'] = '𝗌';
   1.355 +utf8['\\<Leftrightarrow>'] = '⇔';
   1.356 +utf8['\\<heartsuit>'] = '♡';
   1.357 +utf8['\\<four>'] = '𝟰';
   1.358 +
   1.359 +var re_xsymbol = /\\<.*?>/g;
   1.360 +
   1.361 +function encodequery(ele) {
   1.362 +  var text = ele.value;
   1.363 +  var otext = text;
   1.364 +  var pos = getCaret(ele);
   1.365 +
   1.366 +  xsymbols = text.match(re_xsymbol);
   1.367 +  for (i in xsymbols) {
   1.368 +    var repl = utf8[xsymbols[i]];
   1.369 +    if (repl) {
   1.370 +	text = text.replace(xsymbols[i], repl, "g");
   1.371 +    }
   1.372 +  }
   1.373 +
   1.374 +  if (text != otext) {
   1.375 +    ele.value = text;
   1.376 +
   1.377 +    if (pos != -1) {
   1.378 +      pos = pos - (otext.length - text.length);
   1.379 +      setCaret(ele, pos);
   1.380 +    }
   1.381 +  }
   1.382 +}
   1.383 +
   1.384 +/* from: http://www.webdeveloper.com/forum/showthread.php?t=74982 */
   1.385 +function getCaret(obj) {
   1.386 +  var pos = -1;
   1.387 +
   1.388 +  if (document.selection) { // IE
   1.389 +    obj.focus ();
   1.390 +    var sel = document.selection.createRange();
   1.391 +    var sellen = document.selection.createRange().text.length;
   1.392 +    sel.moveStart ('character', -obj.value.length);
   1.393 +    pos = sel.text.length - sellen;
   1.394 +
   1.395 +  } else if (obj.selectionStart || obj.selectionStart == '0') { // Gecko
   1.396 +    pos = obj.selectionStart;
   1.397 +  }
   1.398 +  
   1.399 +  return pos;
   1.400 +}
   1.401 +
   1.402 +/* from: http://parentnode.org/javascript/working-with-the-cursor-position/ */
   1.403 +function setCaret(obj, pos) {
   1.404 +  if (obj.createTextRange) {
   1.405 +      var range = obj.createTextRange();
   1.406 +      range.move("character", pos);
   1.407 +      range.select();
   1.408 +  } else if (obj.selectionStart) {
   1.409 +      obj.focus();
   1.410 +      obj.setSelectionRange(pos, pos);
   1.411 +  }
   1.412 +}
   1.413 +