src/Tools/WWW_Find/www/find_theorems.js

make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;

/*
 * 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['\\<twosuperior>'] = '²';
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['\\<threesuperior>'] = '³';
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['\\<onesuperior>'] = '¹';
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);
  }
}