]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/index.html
d26024e56a08d6b045a812c32eb5f2f87d5d74a7
[helm.git] / helm / searchEngine / html / index.html
1 <HTML>
2 <HEAD>
3 <SCRIPT language="Javascript">
4 var query="*"; // stringa che contiene la query nel suo stato attuale.
5 var storeps=1;
6 var storepv=1;
7 var storepb=1; // queste tre variabili contengono il numero da assegnare al prossimo simbolo set, val o boole per creare il link nel frame in alto a sinistra.
8 var stadd; // contiene la stringa da aggiungere alla query.
9 var fb; // contiene la stringa da aggiungere alla query prima che i set,val e boole siano convertiti in link.
10 var ltr="*"; // qui viene memorizzato qual è l' ultimo link su cui si è cliccato.
11 var norvars=0;
12 var nosvars=0;
13 var novvars1=0;
14 var novvars2=0; // queste tre variabili servono per sapere dove memorizzare i nomi delle rvar,svar e vvar inserite dall' utente. 
15 var wrong=0;
16 var ricordaliaslist=0;
17 var actinput=0;
18 var numeroazioniannullate=0;
19 var terminecic="";var listaliases="";vlds=new Array();//contengono i parametri per dialogare col server in caso di ambiguità nella Match Conclusion.
20 var disambiguation_choices = "";
21 aliasglob=new Array();//per conservare la lista degli alias
22 function initialize()
23         {
24         rvars=new Array(100);
25         svars=new Array(100);
26         vvars1=new Array(100);
27         vvars2=new Array(100); // contengono le rvar,svar e vvar inserite dall' utente. 
28         storia=new Array();
29         storia[0]="*";
30         norvars=0;
31         nosvars=0;
32         novvars1=0;
33         novvars2=0;
34         ltr="*";
35         query="*";
36         storeps=1;
37         storepv=1;
38         storepb=1;
39         ricordaliaslist=0;
40         vlds=new Array();
41         aliasglob=new Array();
42         actinput=0;
43         numeroazioniannullate=0;
44         }
45 function help(w) // quando invocata, visualizza l' help relativo ad un oggetto. Di solito è legata ad un evento onFocus o onMouseOver.  
46         {
47         hw.document.close();
48         switch (w)      {
49                         case -9: hw.document.write("By clicking this you may add or remove aliases as you wish.")
50                                 break;
51                         case -81: hw.document.write("Allows you to recover your last input")
52                                 break;
53                         case -8: hw.document.write("Allows you to delete your last input")
54                                 break;
55                         case -7: hw.document.write("Erases your query and starts a new pre-defined query.")
56                                 break;
57                         case -6: hw.document.write("Puts this string in the current cursor position. This button works only with Internet Explorer.")
58                                 break;
59                         case -5: hw.document.write("Erases your query and starts a new one.")
60                                 break;
61                         case -4: hw.document.write("If you click this your query will be processed and the results will appear in the frame above.")
62                                 break;
63                         case -3: hw.document.write("Substitutes your query with the text written in the area above. Unless you have a good knowledge of MathQL, it's recommended that you use this only to recover errors.")
64                                 break;
65                         case -2: hw.document.write("This is the edit/submit window. You can modify your query here, but be aware that no syntax check will be performed and that if you enter a <a href=grammar.html#rvar target=gw>variable</a> it won't be available for quick composition later. You may also want to add a <a href=grammar.html#set target=gw>set</a>, a <a href=grammar.html#val target=gw>val</a> or a <a href=grammar.html#boole target=gw>boole</a> somewhere in the query. If you do, write '&lt;set&gt;','&lt;val&gt;' or '&lt;bol&gt;' in the point you'd like it to appear, or use the buttons on the right if you are using IE. When you're done with the query, click the Submit button.")
66                                 break;
67                         case -1: hw.document.write("You may see the grammar here.")
68                                 break;
69                         case 0: hw.document.write("")
70                                 break;
71                         case 1: hw.document.write("You may enter an arbitrary statement here; be careful since syntax errors won't be detected.");                              
72                                 break;  
73                         case 2: hw.document.write("Enter an <a href=grammar.html#attr_list target=gw>attr_list</a> here.");
74                                 break;
75                         case 3: hw.document.write("Enter an <a href=grammar.html#id target=gw>id</a> here.");
76                                 break;
77                         case 4: hw.document.write("You must select one previously entered <a href=grammar.html#rvar target=gw>rvar</a>. If you haven't already entered at least one, you can't choose this. ");
78                                 break;
79                         case 5: hw.document.write("Enter a <a href=grammar.html#path target=gw>path</a> here.");
80                                 break;
81                         case 6: hw.document.write("You must select one previously entered <a href=grammar.html#svar target=gw>svar</a>. If you haven't already entered at least one, you can't choose this. ");
82                                 break;
83                         case 7: hw.document.write("Enter a <a href=grammar.html#string_list target=gw>string_list</a> here.");
84                                 break;
85                         case 8: hw.document.write("You must select one <a href=grammar.html#vvar target=gw>vvar</a> previously entered as an 'attr'. If you haven't already entered at least one, you can't choose this. ");
86                                 break;
87                         case 81: hw.document.write("You must select one <a href=grammar.html#vvar target=gw>vvar</a> previously entered in a 'let' statement. If you haven't already entered at least one, you can't choose this. ");
88                                 break;
89                         case 9: hw.document.write("Enter a single <a href=grammar.html#quoted_string target=gw>quoted_string</a> here.");
90                                 break;
91                         }       
92         }
93 function tpa(quotpath)
94         {
95         while (quotpath.indexOf("<")>-1)
96                 {quotpath=quotpath.replace("<","&lt;");}
97         while (quotpath.indexOf(">")>-1)
98                 {quotpath=quotpath.replace(">","&gt;");}
99         return (quotpath);
100         }
101 function gramcheck(how,what) // esegue il controllo sintattico sulla stringa "what", controllando che rispetti i requisiti indicati dalla clausola "how". Se qualcosa non è ok, la variabile "wrong" viene posta ad 1 e la stringa da aggiungere viene ignorata, mentre viene visualizzato un apposito messaggio di errore.              
102         {
103         var slash=0;
104         var alpha=/[A-Za-z:_]/
105         var numero=/[0-9]/
106         switch (how)    {               
107                         case "qsl": // lista di quoted string
108                                 if (what.charAt(0)!="{") {gramcheck("qs",what);break;}
109                                 if (what.charAt(what.length-1)!="}") {alert ("The list must end with a '}'.");wrong=1;break;}
110                                 what=what.substring(1,what.length-1);//alert (what);
111                                 while (what.indexOf("\",\"")>-1)
112                                         {
113                                         as=what.substring(0,what.indexOf("\",\"")+1);//alert(as);
114                                         what=what.substring(what.indexOf("\",\"")+2,what.length);//alert(what);
115                                         gramcheck("qs",as);
116                                         }
117                                 gramcheck("qs",what);
118                                 break;
119                         case "qp": // quoted path
120                                 if (what.charAt(0)!="\"") {alert ("A quoted string must be included between quotes."); wrong=1; break;}
121                                 if (what.charAt(what.length-1)!="\"") {alert ("A quoted string must be included between quotes."); wrong=1; break;}
122                                 while (what.indexOf("\"/\"")>-1)
123                                         {
124                                         as=what.substring(0,what.indexOf("\"/\"")+1);//alert(as);
125                                         what=what.substring(what.indexOf("\"/\"")+2,what.length);//alert(what);
126                                         gramcheck("qs",as);
127                                         }
128                                 gramcheck("qs",what);
129                                 break;
130                         case "qs": // quoted string
131                                 if (what.charAt(0)!="\"") {alert ("A quoted string must be included between quotes."); wrong=1; break;}
132                                 if (what.charAt(what.length-1)!="\"") {alert ("A quoted string must be included between quotes."); wrong=1; break;}
133                                 what=what.substring(0,what.length-1);//alert (what);
134                                 if (wrong==1) break;
135                                 else while (what.length>0)
136                                         {
137                                         what=what.substring(1,what.length);
138                                         if (what.charAt(0)=="\"" && slash==0) {alert ("A \" in a quoted string must be preceded by a \\.");wrong=1;break;} 
139                                         if (what.charAt(0)=="\\") {slash=1} else {slash=0} 
140                                         if (slash==1 && what.length==1) {alert ("A \\ in a quoted string must be followed by something.");wrong=1;}
141                                         }
142                                 break;
143                         case "vlist": // lista di vvar (tutto ciò che si trova dopo "attr")
144                                 //alert(what.substring(0,4));                           
145                                 if ((what.substring(0,4))!="attr"){wrong=1;alert("A vvar_list must begin with the word 'attr'")}
146                                 what=what.substring(5,(what.length));vl=what;
147                                 //alert(what+"what");
148                                 while (what.length>0)
149                                                         {
150                                                         if (what.indexOf(",")>0) {vv=(what.substring(0,what.indexOf(",")));}
151                                                         else {vv=what}                                  
152                                 //alert(vv+"vv");
153                                                         if (vv.charAt(0)!="$"){wrong=1;alert("A vvar must begin with a '$'");}
154                                                         if (vv.indexOf("<-")>0)
155                                                                         {
156                                                                         what=what.substring(vv.length+1,what.length);
157                                 //alert(what+" nuovowhat "+wrong);
158                                                                         path=vv.substring(vv.indexOf("<-")+2,vv.length);
159                                 //alert(path+" path "+wrong);
160                                                                         gramcheck("qp",path); 
161                                                                         vv=vv.substring(1,(vv.indexOf("<-")));
162                                 //alert(vv+" vv "+wrong);
163                                                                         gramcheck("id",vv);
164                                                                         }
165                                                         else {wrong=1;alert("An Assign must contain a '<-'.");what="";}
166                                 //alert (what+"what");  
167                                                         }
168                                 break;
169                         case "id":
170                                 //alert (what.charAt(0));
171                                 if (!alpha.test(what.charAt(0))) {wrong=1;alert("An ID must begin with a letter , ':' , or '_' .");}
172                                 while (what.length>1)   {
173                                         what=what.substring(1,(what.length));
174                                         if (!alpha.test(what.charAt(0)) && !numero.test(what.charAt(0)))
175                                         {wrong=1;alert(what.charAt(0)+" is not a valid character for an id.");}
176                                         //document.write(what+"<BR>");
177                                                         }       
178                                 break;
179                         }
180         
181         if (how=="vlist" && wrong==0) // nel caso in cui sia stato eseguito il controllo su una lista di vvar e non siano stati riscontrati errori, tutte le variabili inserite vengono memorizzate.
182                 {
183                 while (vl.length>0)
184                         {
185                         if (vl.indexOf(",")>-1)
186                                 {
187                                 vvars2[novvars2++]=vl.substring(0,vl.indexOf("<"));
188                                 vl=vl.substring(vl.indexOf(",")+1,vl.length);
189                                 }
190                         else    
191                                 {
192                                 vvars2[novvars2++]=vl.substring(0,vl.indexOf("<"));;
193                                 vl="";
194                                 }                                               
195                         }
196                 //alert ("esco dal loop");
197                 }
198         if (wrong==0) {cw.inputok=1} else stadd="";
199         }
200 function savelink(n,t) // invocata quando si clicca su un link, memorizza quale di questi debba poi essere sostituito. 
201         {
202         if (t=='s') { top.ltr="[?set"+String(n)+"]";}
203         if (t=='v') { top.ltr="[?val"+String(n)+"]";}
204         if (t=='b') { top.ltr="[?bol"+String(n)+"]";}
205 //      alert(ltr);
206         }
207 function aggcw() // invocata automaticamente ad ogni modifica della variabile "query", fa apparire nel frame in alto a destra il menu di composizione relativo al primo link della query. Consente quindi di comporre tutta la query senza mai cliccare su alcun link. 
208         {
209         pq=query;
210         while (pq.length>0)
211                 {
212                 if (pq.indexOf("[?")>-1)        
213                         {
214                         ltr=pq.slice(pq.indexOf("[?"));
215                         ltr=ltr.substring(ltr.indexOf("[?"),(ltr.length-ltr.indexOf("[?"))-(ltr.length-ltr.indexOf("]")-1));
216                         wto=ltr.substring(2,5);
217                         if (wto=="set") {window.open(top.topurl+"/getpage?url=set.html","cw");pq="";}
218                         else if (wto=="val") {window.open(top.topurl+"/getpage?url=val.html","cw");pq="";}
219                         else if (wto=="bol") {window.open(top.topurl+"/getpage?url=boole.html","cw");pq="";}
220                         else pq=pq.substring(pq.indexOf("[?")+2,pq.length);
221                         }
222                 else {window.open(top.topurl+"/getpage?url=blank.html","cw");pq="";}
223                 } 
224         }
225 function aggform() // aggiorna il form nel frame centrale. Invocata ad ogni cambio della variabile "query".
226         {
227         cquery=query;
228         while (cquery.indexOf("<")>-1)
229                 {
230                 cquery=cquery.replace(cquery.substring(cquery.indexOf("<"),cquery.indexOf(">")+1),"");
231                 //alert(cquery);
232                 }
233         while (cquery.indexOf("[?")>-1)
234                 {
235                 //alert(cquery);
236                 if (cquery.indexOf("]")>-1)
237                         {
238                         while (cquery.indexOf("]")<cquery.indexOf("[?") && cquery.indexOf("]")>-1)
239                         {cquery=cquery.replace("]","q+u+a+d+r+a+c+h+i+u+s+a");}//alert("loop"+cquery.indexOf("]")+cquery.indexOf("[?"))}
240                         ag1=cquery.slice(cquery.indexOf("[?"));//alert(ag1);
241                         ag1=ag1.substring(ag1.indexOf("[?"),(ag1.length-ag1.indexOf("[?"))-(ag1.length-ag1.indexOf("]")));//alert(ag1);
242                         ag2=ag1.substring(2,5);//alert(ag2);
243                         if (ag2=="set") cquery=cquery.replace(cquery.substring(cquery.indexOf("[?"),cquery.indexOf("]")+1),"<set>");
244                         else if (ag2=="val") cquery=cquery.replace(cquery.substring(cquery.indexOf("[?"),cquery.indexOf("]")+1),"<val>");
245                         else if (ag2=="bol") cquery=cquery.replace(cquery.substring(cquery.indexOf("[?"),cquery.indexOf("]")+1),"<boole>");
246                         else cquery=cquery.replace(cquery.substring(cquery.indexOf("[?"),cquery.indexOf("[?")+1),"q+u+a+d+r+a");
247                         //alert(cquery);
248                         }
249                 else {cquery=cquery.replace("[?","q+u+a+d+r+a?")}
250                 //alert(cquery);        
251                 }
252         while (cquery.indexOf("q+u+a+d+r+a+c+h+i+u+s+a")>-1)
253                 {
254                 cquery=cquery.replace("q+u+a+d+r+a+c+h+i+u+s+a","]");
255                 }
256         while (cquery.indexOf("q+u+a+d+r+a")>-1)
257                 {
258                 cquery=cquery.replace("q+u+a+d+r+a","[");
259                 }
260         while (cquery.indexOf("&lt;")>-1)
261                 {
262                 cquery=cquery.replace("&lt;","<");
263                 }
264         while (cquery.indexOf("&gt;")>-1)
265                 {
266                 cquery=cquery.replace("&gt;",">");
267                 }
268         top.sw.agg();
269         }
270 function ripristina()
271         {
272         //alert (actinput+" "+storia.length);
273         if (numeroazioniannullate>0)
274                 {
275                 numeroazioniannullate--;
276                 query=storia[actinput+1];actinput++;
277                 qw.document.close();
278                 qw.document.write(query);
279                 aggform();
280                 sw.apply();
281                 aggcw();
282                 cw.focus();
283                 }
284         }
285 function annulla()
286         {
287         //alert (actinput+" "+storia.length);
288         if (actinput>0)
289                 {
290                 numeroazioniannullate++;
291                 query=storia[actinput-1];actinput--;
292                 qw.document.close();
293                 qw.document.write(query);
294                 aggform();
295                 sw.apply();
296                 if (query=="*"){cw.location=top.topurl+"/getpage?url=set.html";ltr="*";} else {aggcw();}
297                 cw.focus();
298                 }
299         }
300 function parse() // prende la stringa che si sta tentando di inserire nella query, aggiunge i link dove necessario e mette il risultato nella variabile "fb"
301         {
302         while (fb.indexOf("[set]")>-1){
303         if (fb.indexOf("set")>0)
304                 {
305       fb=fb.replace("[set]","<A HREF="+top.topurl+"/getpage?url=set.html target=cw onclick=top.savelink("+top.storeps+",'s')>[?set"+top.storeps+"]</A>");
306                 top.storeps++;
307                 }
308                                          }
309         while (fb.indexOf("[val]")>-1){
310         if (fb.indexOf("val")>0)
311                 {
312       fb=fb.replace("[val]","<A HREF="+top.topurl+"/getpage?url=val.html target=cw onclick=top.savelink("+top.storepv+",'v')>[?val"+top.storepv+"]</A>");
313                 top.storepv++;
314                 }
315                                          }
316         while (fb.indexOf("[boole]")>-1){
317         if (fb.indexOf("boole")>0)
318                 {
319                 fb=fb.replace("[boole]","<A HREF="+top.topurl+"/getpage?url=boole.html target=cw onclick=top.savelink("+top.storepb+",'b')>[?bol"+top.storepb+"]</A>");
320                 top.storepb++;
321                 }
322                                          }
323         }
324 function aggq() // aggiorna la query sostituendo l' ultimo link editato con la stringa inserita, poi aggiorna tutti i frame.
325         {
326         //window.open(top.topurl+"/getpage?url=summary.html","cw");
327         qw.document.close();
328         fb=stadd;       
329         nst=ltr.substring(5,(ltr.length-1));// alert(nst+" "+ltr);
330         query=query.replace("<A HREF="+top.topurl+"/getpage?url=set.html target=cw onclick=top.savelink("+nst+",'s')>"+ltr+"</A>",ltr);
331         query=query.replace("<A HREF="+top.topurl+"/getpage?url=val.html target=cw onclick=top.savelink("+nst+",'v')>"+ltr+"</A>",ltr);
332         query=query.replace("<A HREF="+top.topurl+"/getpage?url=boole.html target=cw onclick=top.savelink("+nst+",'b')>"+ltr+"</A>",ltr);
333         parse();
334         query=query.replace(ltr,fb);
335         actinput++;storia[actinput]=query;numeroazioniannullate=0;//alert (actinput+" "+storia.length);
336         qw.document.write(query);aggform();
337         aggcw();
338         cw.focus();
339         }
340   var topurl=document.location.protocol+'//'+document.location.host;
341 </SCRIPT>
342 </HEAD>
343   <script>
344     document.write(' <FRAMESET ROWS="69%,31%"> <FRAMESET COLS="40%,60%"> <FRAMESET ROWS="46%,54%"> <FRAME NAME="qw" SRC="'+topurl+'/getpage?url=start.html"> <FRAME NAME="sw" SRC="'+topurl+'/getpage?url=blank.html"> </FRAMESET> <FRAME NAME="cw" SRC="'+topurl+'/getpage?url=blank.html"> </FRAMESET> <FRAMESET COLS="49%,51%"> <FRAME NAME="gw" SRC="'+topurl+'/getpage?url=blank.html" onFocus="help(-1)";> <FRAME NAME="hw" SRC="'+topurl+'/getpage?url=blank.html"> </FRAMESET> </FRAMESET>');
345   </script>
346 </HTML>