]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/editor.html
use new METAS/* names
[helm.git] / helm / searchEngine / html / editor.html
1 <HTML>
2 <HEAD>
3 <SCRIPT language="Javascript">
4 qbf=/[[^\[\]<>]*|<set>|<val>|<boole>]*/
5 function invia()
6         {
7         window.open(top.ask_uwobo(top.topurl+"/execute?query="+escape(document.edit.qta.value)),"cw");
8         }
9 function parse1()
10         {
11         while (fb.indexOf("<")>-1){
12         if (fb.indexOf("<")>0)
13                 {
14                 fb=fb.replace("<","&lt;");
15                 }
16                                          }
17         while (fb.indexOf(">")>-1){
18         if (fb.indexOf(">")>0)
19                 {
20                 fb=fb.replace(">","&gt;");
21                 }
22                                          }
23         //while (fb.indexOf("[?")>-1){
24                 //fb=fb.replace("[?","&gt;");
25                         //               }
26         }
27 function parse()
28         {
29         while (fb.indexOf("<set>")>-1)
30                 {
31                 fb=fb.replace("<set>","[set]");
32                 }
33         while (fb.indexOf("<val>")>-1)
34                 {
35                 fb=fb.replace("<val>","[val]");
36                 }
37         while (fb.indexOf("<boole>")>-1)
38                 {
39                 fb=fb.replace("<boole>","[boole]");
40                 }
41         parse1();
42         }
43 function armageddon()
44         {
45         if (confirm("This will delete your query and restart a new one. Are you sure?")) {
46         top.initialize();
47         top.window.open(top.topurl+top.action+"start.html","qw");
48         top.window.open(top.topurl+top.action+"blank.html","cw");
49         top.window.open(top.topurl+top.action+"blank.html","hw");
50         top.window.open(top.topurl+top.action+"blank.html","gw");
51         top.window.open(top.topurl+top.action+"blank.html","sw");
52         }
53         }
54 function comprimispazi()
55         {
56         stringa=document.edit.qta.value;
57         while (stringa.charAt(0)==" ") {stringa=stringa.substring(1,stringa.length)}
58         sle=stringa.length;
59         for (i=1;i<sle;i++)
60                 {
61                 if (stringa.charAt(i)==" " && stringa.charAt(i+1)==" ") {
62                         //alert("i="+i+"char="+stringa.charAt(i));
63                         //alert(stringa.substring(0,i)+"---"+stringa.substring(i+1,stringa.length));
64                         stringa=stringa.substring(0,i)+stringa.substring(i+1,stringa.length); i--;}             
65                 }
66         document.edit.qta.value=stringa;
67         }
68 function apply()
69         {
70         top.storep=1;
71         fb=document.edit.qta.value;
72         ok=qbf.test(fb);
73         if (ok){
74         parse();
75         //alert("parse ok");
76         top.fb=fb;
77         top.storeps=1;top.storepv=1;top.storepb=1;
78         top.parse();
79         //alert("top.parse ok");
80         top.query=top.fb;
81         top.qw.document.close();
82         top.qw.document.write(top.query);
83         top.aggform();  //alert("aggform ok");
84         top.aggcw();//alert("aggcw ok");
85         comprimispazi();}
86         }
87 function inserisci(mq)
88         {
89         document.edit.qta.focus();
90         var TR=document.selection.createRange();
91         if(TR!=null)
92                 {
93                         TR.text=TR.text+mq;
94                 } 
95         else document.edit.qta.value+=mq;
96         //comprimispazi();
97         }
98 function agg()
99         {
100         document.edit.qta.value=top.cquery;
101         comprimispazi();
102         }
103 </SCRIPT>
104 </HEAD>
105 <BODY>
106 <table>
107 <tr><td>
108 <form name="edit" method="get" action="Javascript:invia()">
109 <textarea name="qta" cols="40" rows="8" onMouseOver="top.help(-2)";>
110 </textarea>
111 </td>
112 <td>
113 <input type="button" value="set" onMouseOver="top.help(-6)" onClick="inserisci(' <set> ');"><br>
114 <input type="button" value="val" onMouseOver="top.help(-6)" onClick="inserisci(' <val> ');"><br>
115 <input type="button" value="bol" onMouseOver="top.help(-6)" onClick="inserisci(' <boole> ');"><br>
116 </td></tr></table>
117 <input type="submit" value="Submit the query" onMouseOver="top.help(-4)"></input>
118 <input type="button" value="Restart" onMouseOver="top.help(-5)" onClick="armageddon()"></input>
119 <input type="button" value="Apply Changes" onMouseOver="top.help(-3)" onClick="apply();top.actinput++;top.storia[top.actinput]=top.query;top.numeroazioniannullate=0;"></input>
120 </form>
121 </BODY>
122 </HTML>