src/Tools/WWW_Find/www/find_theorems.js

--- a/src/Tools/WWW_Find/www/find_theorems.js	Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,406 +0,0 @@
-/*
- * Author: Timothy Bourke, NICTA
- */
-var utf8 = new Object();
-utf8['\\<supseteq>'] = '⊇';
-utf8['\\<KK>'] = '𝔎';
-utf8['\\<up>'] = '↑';
-utf8['\\<otimes>'] = '⊗';
-utf8['\\<aa>'] = '𝔞';
-utf8['\\<dagger>'] = '†';
-utf8['\\<frown>'] = '⌢';
-utf8['\\<guillemotleft>'] = '«';
-utf8['\\<qq>'] = '𝔮';
-utf8['\\<X>'] = '𝒳';
-utf8['\\<triangleright>'] = '▹';
-utf8['\\<guillemotright>'] = '»';
-utf8['\\<nu>'] = 'ν';
-utf8['\\<sim>'] = '∼';
-utf8['\\<rightharpoondown>'] = '⇁';
-utf8['\\<p>'] = '𝗉';
-utf8['\\<Up>'] = '⇑';
-utf8['\\<triangleq>'] = '≜';
-utf8['\\<nine>'] = '𝟵';
-utf8['\\<preceq>'] = '≼';
-utf8['\\<nabla>'] = '∇';
-utf8['\\<FF>'] = '𝔉';
-utf8['\\<II>'] = 'ℑ';
-utf8['\\<VV>'] = '𝔙';
-utf8['\\<and>'] = '∧';
-utf8['\\<mapsto>'] = '↦';
-utf8['\\<ll>'] = '𝔩';
-utf8['\\<F>'] = 'ℱ';
-utf8['\\<degree>'] = '°';
-utf8['\\<beta>'] = 'β';
-utf8['\\<Colon>'] = '∷';
-utf8['\\<bool>'] = '𝔹';
-utf8['\\<e>'] = '𝖾';
-utf8['\\<lozenge>'] = '◊';
-utf8['\\<u>'] = '𝗎';
-utf8['\\<sharp>'] = '♯';
-utf8['\\<Longleftrightarrow>'] = '⟺';
-utf8['\\<Otimes>'] = '⨂';
-utf8['\\<EE>'] = '𝔈';
-utf8['\\<I>'] = 'ℐ';
-utf8['\\<UU>'] = '𝔘';
-utf8['\\<exclamdown>'] = '¡';
-utf8['\\<dots>'] = '…';
-utf8['\\<N>'] = '𝒩';
-utf8['\\<kk>'] = '𝔨';
-utf8['\\<plusminus>'] = '±';
-utf8['\\<E>'] = 'ℰ';
-utf8['\\<triangle>'] = '△';
-utf8['\\<eta>'] = 'η';
-utf8['\\<triangleleft>'] = '◃';
-utf8['\\<chi>'] = 'χ';
-utf8['\\<z>'] = '𝗓';
-utf8['\\<hungarumlaut>'] = '˝';
-utf8['\\<partial>'] = '∂';
-utf8['\\<three>'] = '𝟯';
-utf8['\\<lesssim>'] = '≲';
-utf8['\\<subset>'] = '⊂';
-utf8['\\<H>'] = 'ℋ';
-utf8['\\<leftarrow>'] = '←';
-utf8['\\<PP>'] = '𝔓';
-utf8['\\<sqsupseteq>'] = '⊒';
-utf8['\\<R>'] = 'ℛ';
-utf8['\\<bowtie>'] = '⨝';
-utf8['\\<C>'] = '𝒞';
-utf8['\\<ddagger>'] = '‡';
-utf8['\\<ff>'] = '𝔣';
-utf8['\\<turnstile>'] = '⊢';
-utf8['\\<bar>'] = '¦';
-utf8['\\<propto>'] = '∝';
-utf8['\\<S>'] = '𝒮';
-utf8['\\<vv>'] = '𝔳';
-utf8['\\<lhd>'] = '⊲';
-utf8['\\<paragraph>'] = '¶';
-utf8['\\<mu>'] = 'μ';
-utf8['\\<rightharpoonup>'] = '⇀';
-utf8['\\<Inter>'] = '⋂';
-utf8['\\<o>'] = '𝗈';
-utf8['\\<asymp>'] = '≍';
-utf8['\\<Leftarrow>'] = '⇐';
-utf8['\\<Sqinter>'] = '⨅';
-utf8['\\<eight>'] = '𝟴';
-utf8['\\<succeq>'] = '≽';
-utf8['\\<forall>'] = '∀';
-utf8['\\<complex>'] = 'ℂ';
-utf8['\\<GG>'] = '𝔊';
-utf8['\\<Coprod>'] = '∐';
-utf8['\\<L>'] = 'ℒ';
-utf8['\\<WW>'] = '𝔚';
-utf8['\\<leadsto>'] = '↝';
-utf8['\\<D>'] = '𝒟';
-utf8['\\<angle>'] = '∠';
-utf8['\\<section>'] = '§';
-utf8['\\<TTurnstile>'] = '⊫';
-utf8['\\<mm>'] = '𝔪';
-utf8['\\<T>'] = '𝒯';
-utf8['\\<alpha>'] = 'α';
-utf8['\\<leftharpoondown>'] = '↽';
-utf8['\\<rho>'] = 'ρ';
-utf8['\\<wrong>'] = '≀';
-utf8['\\<l>'] = '𝗅';
-utf8['\\<doteq>'] = '≐';
-utf8['\\<times>'] = '×';
-utf8['\\<noteq>'] = '≠';
-utf8['\\<rangle>'] = '⟩';
-utf8['\\<div>'] = '÷';
-utf8['\\<Longrightarrow>'] = '⟹';
-utf8['\\<BB>'] = '𝔅';
-utf8['\\<sqsupset>'] = '⊐';
-utf8['\\<rightarrow>'] = '→';
-utf8['\\<real>'] = 'ℝ';
-utf8['\\<hh>'] = '𝔥';
-utf8['\\<Phi>'] = 'Φ';
-utf8['\\<integral>'] = '∫';
-utf8['\\<CC>'] = 'ℭ';
-utf8['\\<euro>'] = '€';
-utf8['\\<xx>'] = '𝔵';
-utf8['\\<Y>'] = '𝒴';
-utf8['\\<zeta>'] = 'ζ';
-utf8['\\<longleftarrow>'] = '⟵';
-utf8['\\<a>'] = '𝖺';
-utf8['\\<onequarter>'] = '¼';
-utf8['\\<And>'] = '⋀';
-utf8['\\<downharpoonright>'] = '⇂';
-utf8['\\<phi>'] = 'φ';
-utf8['\\<q>'] = '𝗊';
-utf8['\\<Rightarrow>'] = '⇒';
-utf8['\\<clubsuit>'] = '♣';
-utf8['\\<ggreater>'] = '≫';
-utf8['\\<two>'] = '𝟮';
-utf8['\\<succ>'] = '≻';
-utf8['\\<AA>'] = '𝔄';
-utf8['\\<lparr>'] = '⦇';
-utf8['\\<Squnion>'] = '⨆';
-utf8['\\<HH>'] = 'ℌ';
-utf8['\\<sqsubseteq>'] = '⊑';
-utf8['\\<QQ>'] = '𝔔';
-utf8['\\<setminus>'] = '∖';
-utf8['\\<Lambda>'] = 'Λ';
-utf8['\\<RR>'] = 'ℜ';
-utf8['\\<J>'] = '𝒥';
-utf8['\\<gg>'] = '𝔤';
-utf8['\\<hyphen>'] = '­';
-utf8['\\<B>'] = 'ℬ';
-utf8['\\<Z>'] = '𝒵';
-utf8['\\<ww>'] = '𝔴';
-utf8['\\<lambda>'] = 'λ';
-utf8['\\<onehalf>'] = '½';
-utf8['\\<f>'] = '𝖿';
-utf8['\\<Or>'] = '⋁';
-utf8['\\<v>'] = '𝗏';
-utf8['\\<natural>'] = '♮';
-utf8['\\<seven>'] = '𝟳';
-utf8['\\<Oplus>'] = '⨁';
-utf8['\\<subseteq>'] = '⊆';
-utf8['\\<rfloor>'] = '⌋';
-utf8['\\<LL>'] = '𝔏';
-utf8['\\<Sum>'] = '∑';
-utf8['\\<ominus>'] = '⊖';
-utf8['\\<bb>'] = '𝔟';
-utf8['\\<Pi>'] = 'Π';
-utf8['\\<cent>'] = '¢';
-utf8['\\<diamond>'] = '◇';
-utf8['\\<mho>'] = '℧';
-utf8['\\<O>'] = '𝒪';
-utf8['\\<rr>'] = '𝔯';
-utf8['\\<leftharpoonup>'] = '↼';
-utf8['\\<pi>'] = 'π';
-utf8['\\<k>'] = '𝗄';
-utf8['\\<star>'] = '⋆';
-utf8['\\<rightleftharpoons>'] = '⇌';
-utf8['\\<equiv>'] = '≡';
-utf8['\\<langle>'] = '⟨';
-utf8['\\<Longleftarrow>'] = '⟸';
-utf8['\\<nexists>'] = '∄';
-utf8['\\<Odot>'] = '⨀';
-utf8['\\<lfloor>'] = '⌊';
-utf8['\\<sqsubset>'] = '⊏';
-utf8['\\<SS>'] = '𝔖';
-utf8['\\<box>'] = '□';
-utf8['\\<index>'] = 'ı';
-utf8['\\<pounds>'] = '£';
-utf8['\\<Upsilon>'] = 'Υ';
-utf8['\\<ii>'] = '𝔦';
-utf8['\\<hookleftarrow>'] = '↩';
-utf8['\\<P>'] = '𝒫';
-utf8['\\<epsilon>'] = 'ε';
-utf8['\\<yy>'] = '𝔶';
-utf8['\\<h>'] = '𝗁';
-utf8['\\<upsilon>'] = 'υ';
-utf8['\\<x>'] = '𝗑';
-utf8['\\<not>'] = '¬';
-utf8['\\<le>'] = '≤';
-utf8['\\<one>'] = '𝟭';
-utf8['\\<cdots>'] = '⋯';
-utf8['\\<some>'] = 'ϵ';
-utf8['\\<Prod>'] = '∏';
-utf8['\\<NN>'] = '𝔑';
-utf8['\\<squnion>'] = '⊔';
-utf8['\\<dd>'] = '𝔡';
-utf8['\\<top>'] = '⊤';
-utf8['\\<dieresis>'] = '¨';
-utf8['\\<tt>'] = '𝔱';
-utf8['\\<U>'] = '𝒰';
-utf8['\\<unlhd>'] = '⊴';
-utf8['\\<cedilla>'] = '¸';
-utf8['\\<kappa>'] = 'κ';
-utf8['\\<amalg>'] = '⨿';
-utf8['\\<restriction>'] = '↾';
-utf8['\\<struct>'] = '⋄';
-utf8['\\<m>'] = '𝗆';
-utf8['\\<six>'] = '𝟲';
-utf8['\\<midarrow>'] = '─';
-utf8['\\<lbrace>'] = '⦃';
-utf8['\\<lessapprox>'] = '⪅';
-utf8['\\<MM>'] = '𝔐';
-utf8['\\<down>'] = '↓';
-utf8['\\<oplus>'] = '⊕';
-utf8['\\<wp>'] = '℘';
-utf8['\\<surd>'] = '√';
-utf8['\\<cc>'] = '𝔠';
-utf8['\\<bottom>'] = '⊥';
-utf8['\\<copyright>'] = '©';
-utf8['\\<ZZ>'] = 'ℨ';
-utf8['\\<union>'] = '∪';
-utf8['\\<V>'] = '𝒱';
-utf8['\\<ss>'] = '𝔰';
-utf8['\\<unrhd>'] = '⊵';
-utf8['\\<b>'] = '𝖻';
-utf8['\\<downharpoonleft>'] = '⇃';
-utf8['\\<cdot>'] = '⋅';
-utf8['\\<r>'] = '𝗋';
-utf8['\\<Midarrow>'] = '═';
-utf8['\\<Down>'] = '⇓';
-utf8['\\<diamondsuit>'] = '♢';
-utf8['\\<rbrakk>'] = '⟧';
-utf8['\\<lless>'] = '≪';
-utf8['\\<longleftrightarrow>'] = '⟷';
-utf8['\\<prec>'] = '≺';
-utf8['\\<emptyset>'] = '∅';
-utf8['\\<rparr>'] = '⦈';
-utf8['\\<Delta>'] = 'Δ';
-utf8['\\<XX>'] = '𝔛';
-utf8['\\<parallel>'] = '∥';
-utf8['\\<K>'] = '𝒦';
-utf8['\\<nn>'] = '𝔫';
-utf8['\\<registered>'] = '®';
-utf8['\\<M>'] = 'ℳ';
-utf8['\\<delta>'] = 'δ';
-utf8['\\<threequarters>'] = '¾';
-utf8['\\<g>'] = '𝗀';
-utf8['\\<cong>'] = '≅';
-utf8['\\<tau>'] = 'τ';
-utf8['\\<w>'] = '𝗐';
-utf8['\\<ge>'] = '≥';
-utf8['\\<flat>'] = '♭';
-utf8['\\<zero>'] = '𝟬';
-utf8['\\<Uplus>'] = '⨄';
-utf8['\\<longmapsto>'] = '⟼';
-utf8['\\<supset>'] = '⊃';
-utf8['\\<in>'] = '∈';
-utf8['\\<sqinter>'] = '⊓';
-utf8['\\<OO>'] = '𝔒';
-utf8['\\<updown>'] = '↕';
-utf8['\\<circ>'] = '∘';
-utf8['\\<rat>'] = 'ℚ';
-utf8['\\<stileturn>'] = '⊣';
-utf8['\\<ee>'] = '𝔢';
-utf8['\\<Omega>'] = 'Ω';
-utf8['\\<or>'] = '∨';
-utf8['\\<inverse>'] = '¯';
-utf8['\\<rhd>'] = '⊳';
-utf8['\\<uu>'] = '𝔲';
-utf8['\\<iota>'] = 'ι';
-utf8['\\<d>'] = '𝖽';
-utf8['\\<questiondown>'] = '¿';
-utf8['\\<Union>'] = '⋃';
-utf8['\\<omega>'] = 'ω';
-utf8['\\<approx>'] = '≈';
-utf8['\\<t>'] = '𝗍';
-utf8['\\<Updown>'] = '⇕';
-utf8['\\<spadesuit>'] = '♠';
-utf8['\\<five>'] = '𝟱';
-utf8['\\<exists>'] = '∃';
-utf8['\\<rceil>'] = '⌉';
-utf8['\\<JJ>'] = '𝔍';
-utf8['\\<minusplus>'] = '∓';
-utf8['\\<nat>'] = 'ℕ';
-utf8['\\<oslash>'] = '⊘';
-utf8['\\<A>'] = '𝒜';
-utf8['\\<Xi>'] = 'Ξ';
-utf8['\\<currency>'] = '¤';
-utf8['\\<Turnstile>'] = '⊨';
-utf8['\\<hookrightarrow>'] = '↪';
-utf8['\\<pp>'] = '𝔭';
-utf8['\\<Q>'] = '𝒬';
-utf8['\\<aleph>'] = 'ℵ';
-utf8['\\<acute>'] = '´';
-utf8['\\<xi>'] = 'ξ';
-utf8['\\<simeq>'] = '≃';
-utf8['\\<i>'] = '𝗂';
-utf8['\\<Join>'] = '⋈';
-utf8['\\<y>'] = '𝗒';
-utf8['\\<lbrakk>'] = '⟦';
-utf8['\\<greatersim>'] = '≳';
-utf8['\\<greaterapprox>'] = '⪆';
-utf8['\\<longrightarrow>'] = '⟶';
-utf8['\\<lceil>'] = '⌈';
-utf8['\\<Gamma>'] = 'Γ';
-utf8['\\<odot>'] = '⊙';
-utf8['\\<YY>'] = '𝔜';
-utf8['\\<infinity>'] = '∞';
-utf8['\\<Sigma>'] = 'Σ';
-utf8['\\<yen>'] = '¥';
-utf8['\\<int>'] = 'ℤ';
-utf8['\\<tturnstile>'] = '⊩';
-utf8['\\<oo>'] = '𝔬';
-utf8['\\<ointegral>'] = '∮';
-utf8['\\<gamma>'] = 'γ';
-utf8['\\<upharpoonleft>'] = '↿';
-utf8['\\<sigma>'] = 'σ';
-utf8['\\<n>'] = '𝗇';
-utf8['\\<rbrace>'] = '⦄';
-utf8['\\<DD>'] = '𝔇';
-utf8['\\<notin>'] = '∉';
-utf8['\\<j>'] = '𝗃';
-utf8['\\<uplus>'] = '⊎';
-utf8['\\<leftrightarrow>'] = '↔';
-utf8['\\<TT>'] = '𝔗';
-utf8['\\<bullet>'] = '∙';
-utf8['\\<Theta>'] = 'Θ';
-utf8['\\<smile>'] = '⌣';
-utf8['\\<G>'] = '𝒢';
-utf8['\\<jj>'] = '𝔧';
-utf8['\\<inter>'] = '∩';
-utf8['\\<Psi>'] = 'Ψ';
-utf8['\\<ordfeminine>'] = 'ª';
-utf8['\\<W>'] = '𝒲';
-utf8['\\<zz>'] = '𝔷';
-utf8['\\<theta>'] = 'θ';
-utf8['\\<ordmasculine>'] = 'º';
-utf8['\\<c>'] = '𝖼';
-utf8['\\<psi>'] = 'ψ';
-utf8['\\<s>'] = '𝗌';
-utf8['\\<Leftrightarrow>'] = '⇔';
-utf8['\\<heartsuit>'] = '♡';
-utf8['\\<four>'] = '𝟰';
-
-var re_xsymbol = /\\<.*?>/g;
-
-function encodequery(ele) {
-  var text = ele.value;
-  var otext = text;
-  var pos = getCaret(ele);
-
-  xsymbols = text.match(re_xsymbol);
-  for (i in xsymbols) {
-    var repl = utf8[xsymbols[i]];
-    if (repl) {
-	text = text.replace(xsymbols[i], repl, "g");
-    }
-  }
-
-  if (text != otext) {
-    ele.value = text;
-
-    if (pos != -1) {
-      pos = pos - (otext.length - text.length);
-      setCaret(ele, pos);
-    }
-  }
-}
-
-/* from: http://www.webdeveloper.com/forum/showthread.php?t=74982 */
-function getCaret(obj) {
-  var pos = -1;
-
-  if (document.selection) { // IE
-    obj.focus ();
-    var sel = document.selection.createRange();
-    var sellen = document.selection.createRange().text.length;
-    sel.moveStart ('character', -obj.value.length);
-    pos = sel.text.length - sellen;
-
-  } else if (obj.selectionStart || obj.selectionStart == '0') { // Gecko
-    pos = obj.selectionStart;
-  }
-  
-  return pos;
-}
-
-/* from: http://parentnode.org/javascript/working-with-the-cursor-position/ */
-function setCaret(obj, pos) {
-  if (obj.createTextRange) {
-      var range = obj.createTextRange();
-      range.move("character", pos);
-      range.select();
-  } else if (obj.selectionStart) {
-      obj.focus();
-      obj.setSelectionRange(pos, pos);
-  }
-}
-