]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/html/editor.html
Branch V7_3_new_exportation merged.
[helm.git] / helm / searchEngine / html / editor.html
diff --git a/helm/searchEngine/html/editor.html b/helm/searchEngine/html/editor.html
new file mode 100644 (file)
index 0000000..1e6afe7
--- /dev/null
@@ -0,0 +1,122 @@
+<HTML>
+<HEAD>
+<SCRIPT language="Javascript">
+qbf=/[[^\[\]<>]*|<set>|<val>|<boole>]*/
+function invia()
+       {
+       window.open(top.ask_uwobo(top.topurl+"/execute?query="+escape(document.edit.qta.value)),"cw");
+       }
+function parse1()
+       {
+       while (fb.indexOf("<")>-1){
+       if (fb.indexOf("<")>0)
+               {
+               fb=fb.replace("<","&lt;");
+               }
+                                        }
+       while (fb.indexOf(">")>-1){
+       if (fb.indexOf(">")>0)
+               {
+               fb=fb.replace(">","&gt;");
+               }
+                                        }
+       //while (fb.indexOf("[?")>-1){
+               //fb=fb.replace("[?","&gt;");
+                       //               }
+       }
+function parse()
+       {
+       while (fb.indexOf("<set>")>-1)
+               {
+               fb=fb.replace("<set>","[set]");
+               }
+       while (fb.indexOf("<val>")>-1)
+               {
+               fb=fb.replace("<val>","[val]");
+               }
+       while (fb.indexOf("<boole>")>-1)
+               {
+               fb=fb.replace("<boole>","[boole]");
+               }
+       parse1();
+       }
+function armageddon()
+       {
+        if (confirm("This will delete your query and restart a new one. Are you sure?")) {
+       top.initialize();
+       top.window.open(top.topurl+top.action+"start.html","qw");
+       top.window.open(top.topurl+top.action+"blank.html","cw");
+       top.window.open(top.topurl+top.action+"blank.html","hw");
+       top.window.open(top.topurl+top.action+"blank.html","gw");
+       top.window.open(top.topurl+top.action+"blank.html","sw");
+       }
+        }
+function comprimispazi()
+       {
+       stringa=document.edit.qta.value;
+       while (stringa.charAt(0)==" ") {stringa=stringa.substring(1,stringa.length)}
+       sle=stringa.length;
+       for (i=1;i<sle;i++)
+               {
+               if (stringa.charAt(i)==" " && stringa.charAt(i+1)==" ") {
+                       //alert("i="+i+"char="+stringa.charAt(i));
+                       //alert(stringa.substring(0,i)+"---"+stringa.substring(i+1,stringa.length));
+                       stringa=stringa.substring(0,i)+stringa.substring(i+1,stringa.length); i--;}             
+               }
+       document.edit.qta.value=stringa;
+       }
+function apply()
+       {
+       top.storep=1;
+       fb=document.edit.qta.value;
+       ok=qbf.test(fb);
+       if (ok){
+       parse();
+       //alert("parse ok");
+       top.fb=fb;
+       top.storeps=1;top.storepv=1;top.storepb=1;
+       top.parse();
+       //alert("top.parse ok");
+       top.query=top.fb;
+       top.qw.document.close();
+       top.qw.document.write(top.query);
+       top.aggform();  //alert("aggform ok");
+       top.aggcw();//alert("aggcw ok");
+       comprimispazi();}
+       }
+function inserisci(mq)
+       {
+       document.edit.qta.focus();
+       var TR=document.selection.createRange();
+       if(TR!=null)
+               {
+                       TR.text=TR.text+mq;
+               } 
+       else document.edit.qta.value+=mq;
+       //comprimispazi();
+       }
+function agg()
+       {
+       document.edit.qta.value=top.cquery;
+       comprimispazi();
+       }
+</SCRIPT>
+</HEAD>
+<BODY>
+<table>
+<tr><td>
+<form name="edit" method="get" action="Javascript:invia()">
+<textarea name="qta" cols="40" rows="8" onMouseOver="top.help(-2)";>
+</textarea>
+</td>
+<td>
+<input type="button" value="set" onMouseOver="top.help(-6)" onClick="inserisci(' <set> ');"><br>
+<input type="button" value="val" onMouseOver="top.help(-6)" onClick="inserisci(' <val> ');"><br>
+<input type="button" value="bol" onMouseOver="top.help(-6)" onClick="inserisci(' <boole> ');"><br>
+</td></tr></table>
+<input type="submit" value="Submit the query" onMouseOver="top.help(-4)"></input>
+<input type="button" value="Restart" onMouseOver="top.help(-5)" onClick="armageddon()"></input>
+<input type="button" value="Apply Changes" onMouseOver="top.help(-3)" onClick="apply();top.actinput++;top.storia[top.actinput]=top.query;top.numeroazioniannullate=0;"></input>
+</form>
+</BODY>
+</HTML>