]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/index.html
Many changes in the client-side interfaces:
[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 -10: hw.document.write("Insert an <a href=grammarpdq.html#Id target=gw>Id</a> or an <a href=grammarpdq.html#Uri target=gw>Uri</a> here.")
50                                 break;
51                         case -9: hw.document.write("By clicking this you may add or remove aliases as you wish.")
52                                 break;
53                         case -81: hw.document.write("Allows you to recover your last input")
54                                 break;
55                         case -8: hw.document.write("Allows you to delete your last input")
56                                 break;
57                         case -7: hw.document.write("Erases your query and starts a new pre-defined query, you will keep your list of aliases.")
58                                 break;
59                         case -6: hw.document.write("Puts this string in the current cursor position. This button works only with Internet Explorer.")
60                                 break;
61                         case -5: hw.document.write("Erases your query and starts a new one.")
62                                 break;
63                         case -4: hw.document.write("If you click this your query will be processed and the results will appear in the frame above.")
64                                 break;
65                         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.")
66                                 break;
67                         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.")
68                                 break;
69                         case -1: hw.document.write("You may see the grammar here.")
70                                 break;
71                         case 0: hw.document.write("")
72                                 break;
73                         case 1: hw.document.write("You may enter an arbitrary statement here; be careful since syntax errors won't be detected.");                              
74                                 break;  
75                         case 2: hw.document.write("Enter an <a href=grammar.html#attr_list target=gw>attr_list</a> here.");
76                                 break;
77                         case 3: hw.document.write("Enter an <a href=grammar.html#id target=gw>id</a> here.");
78                                 break;
79                         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. ");
80                                 break;
81                         case 5: hw.document.write("Enter a <a href=grammar.html#path target=gw>path</a> here.");
82                                 break;
83                         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. ");
84                                 break;
85                         case 7: hw.document.write("Enter a <a href=grammar.html#string_list target=gw>string_list</a> here.");
86                                 break;
87                         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. ");
88                                 break;
89                         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. ");
90                                 break;
91                         case 9: hw.document.write("Enter a single <a href=grammar.html#quoted_string target=gw>quoted_string</a> here.");
92                                 break;
93                         }       
94         }
95 function tpa(quotpath)
96         {
97         while (quotpath.indexOf("<")>-1)
98                 {quotpath=quotpath.replace("<","&lt;");}
99         while (quotpath.indexOf(">")>-1)
100                 {quotpath=quotpath.replace(">","&gt;");}
101         return (quotpath);
102         }
103 function idcheck(ident)
104         {
105         lettera=/[a-zA-Z]/;
106         partediid=/[a-zA-Z0-9_\-\']/;
107         if (!lettera.test(ident.charAt(0))){alert("an Id must begin with a letter.");return(0)}
108         while (ident.length>0)
109                 {
110                 ident=ident.substring(1,(ident.length));
111                 if (ident.length>0){
112                 if (!partediid.test(ident.charAt(0))){alert(ident.charAt(0)+" is not a valid character for an Id.");return(0);}
113                 }}
114         return(1)
115         }
116 function uricheck(ident)
117         {
118         cifra=/[0-9]/
119         cic=ident.substring(0,5);//alert(cic);
120         if (cic!="cic:/"){alert("an Uri must begin with the string 'cic:/'");return(0);}
121         ident=ident.substring(5,ident.length);//alert(ident);
122         if (ident.indexOf(".")<0){alert("an Uri must contain a '.'");return(0);}
123         ident1=ident.substring(0,ident.indexOf("."));//alert(ident1);
124         ident2=ident.substring(ident.indexOf(".")+1,ident.length);//alert(ident2);
125         while (ident1.length>0)
126                 {       
127                 if (ident1.indexOf("/")>-1)             
128                         {
129                         if (idcheck(ident1.substring(0,ident1.indexOf("/")))==0){return (0)}
130                         ident1=ident1.substring(ident1.indexOf("/")+1,ident1.length);//alert(ident1);
131                         }
132                 else {if (idcheck(ident1)==0){return (0)}       
133                         ident1="";}
134                 }
135         if (ident2=="con"||ident2=="var"){return(1)}
136         if (ident2.substring(0,6)!="ind#1/"){alert ("syntax error in the Uri.");return(0);}
137         ident2=ident2.substring(6,ident2.length);//alert(ident2);
138         if (!cifra.test(ident2.charAt(0))){alert ("syntax error in the Uri.");return(0);}
139         if (ident2.indexOf("/")>-1)
140                 {
141                 while (ident2.charAt(0)!="/")
142                         {
143                         //alert(ident2);
144                         if (!cifra.test(ident2.charAt(0))){alert ("syntax error in the Uri.");return(0);}
145                         ident2=ident2.substring(1,ident2.length);
146                         }
147                 }
148         while (ident2.length>0)
149                 {
150                 //alert(ident2);
151                 ident2=ident2.substring(1,ident2.length);
152                 if (ident2.length>0){
153                 if (!cifra.test(ident2.charAt(0))){alert ("syntax error in the Uri.");return(0);}
154                 }}
155         
156         return(1)
157         }
158 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.              
159         {
160         var slash=0;
161         var alpha=/[A-Za-z:_]/
162         var numero=/[0-9]/
163         switch (how)    {               
164                         case "qsl": // lista di quoted string
165                                 if (what.charAt(0)!="{") {gramcheck("qs",what);break;}
166                                 if (what.charAt(what.length-1)!="}") {alert ("The list must end with a '}'.");wrong=1;break;}
167                                 what=what.substring(1,what.length-1);//alert (what);
168                                 while (what.indexOf("\",\"")>-1)
169                                         {
170                                         as=what.substring(0,what.indexOf("\",\"")+1);//alert(as);
171                                         what=what.substring(what.indexOf("\",\"")+2,what.length);//alert(what);
172                                         gramcheck("qs",as);
173                                         }
174                                 gramcheck("qs",what);
175                                 break;
176                         case "qp": // quoted path
177                                 if (what.charAt(0)!="\"") {alert ("A quoted string must be included between quotes."); wrong=1; break;}
178                                 if (what.charAt(what.length-1)!="\"") {alert ("A quoted string must be included between quotes."); wrong=1; break;}
179                                 while (what.indexOf("\"/\"")>-1)
180                                         {
181                                         as=what.substring(0,what.indexOf("\"/\"")+1);//alert(as);
182                                         what=what.substring(what.indexOf("\"/\"")+2,what.length);//alert(what);
183                                         gramcheck("qs",as);
184                                         }
185                                 gramcheck("qs",what);
186                                 break;
187                         case "qs": // quoted string
188                                 if (what.charAt(0)!="\"") {alert ("A quoted string must be included between quotes."); wrong=1; break;}
189                                 if (what.charAt(what.length-1)!="\"") {alert ("A quoted string must be included between quotes."); wrong=1; break;}
190                                 what=what.substring(0,what.length-1);//alert (what);
191                                 if (wrong==1) break;
192                                 else while (what.length>0)
193                                         {
194                                         what=what.substring(1,what.length);
195                                         if (what.charAt(0)=="\"" && slash==0) {alert ("A \" in a quoted string must be preceded by a \\.");wrong=1;break;} 
196                                         if (what.charAt(0)=="\\") {slash=1} else {slash=0} 
197                                         if (slash==1 && what.length==1) {alert ("A \\ in a quoted string must be followed by something.");wrong=1;}
198                                         }
199                                 break;
200                         case "vlist": // lista di vvar (tutto ciò che si trova dopo "attr")
201                                 //alert(what.substring(0,4));                           
202                                 if ((what.substring(0,4))!="attr"){wrong=1;alert("A vvar_list must begin with the word 'attr'")}
203                                 what=what.substring(5,(what.length));vl=what;
204                                 //alert(what+"what");
205                                 while (what.length>0)
206                                                         {
207                                                         if (what.indexOf(",")>0) {vv=(what.substring(0,what.indexOf(",")));}
208                                                         else {vv=what}                                  
209                                 //alert(vv+"vv");
210                                                         if (vv.charAt(0)!="$"){wrong=1;alert("A vvar must begin with a '$'");}
211                                                         if (vv.indexOf("<-")>0)
212                                                                         {
213                                                                         what=what.substring(vv.length+1,what.length);
214                                 //alert(what+" nuovowhat "+wrong);
215                                                                         path=vv.substring(vv.indexOf("<-")+2,vv.length);
216                                 //alert(path+" path "+wrong);
217                                                                         gramcheck("qp",path); 
218                                                                         vv=vv.substring(1,(vv.indexOf("<-")));
219                                 //alert(vv+" vv "+wrong);
220                                                                         gramcheck("id",vv);
221                                                                         }
222                                                         else {wrong=1;alert("An Assign must contain a '<-'.");what="";}
223                                 //alert (what+"what");  
224                                                         }
225                                 break;
226                         case "id":
227                                 //alert (what.charAt(0));
228                                 if (!alpha.test(what.charAt(0))) {wrong=1;alert("An ID must begin with a letter , ':' , or '_' .");}
229                                 while (what.length>1)   {
230                                         what=what.substring(1,(what.length));
231                                         if (!alpha.test(what.charAt(0)) && !numero.test(what.charAt(0)))
232                                         {wrong=1;alert(what.charAt(0)+" is not a valid character for an id.");}
233                                         //document.write(what+"<BR>");
234                                                         }       
235                                 break;
236                         }
237         
238         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.
239                 {
240                 while (vl.length>0)
241                         {
242                         if (vl.indexOf(",")>-1)
243                                 {
244                                 vvars2[novvars2++]=vl.substring(0,vl.indexOf("<"));
245                                 vl=vl.substring(vl.indexOf(",")+1,vl.length);
246                                 }
247                         else    
248                                 {
249                                 vvars2[novvars2++]=vl.substring(0,vl.indexOf("<"));;
250                                 vl="";
251                                 }                                               
252                         }
253                 //alert ("esco dal loop");
254                 }
255         if (wrong==0) {cw.inputok=1} else stadd="";
256         }
257 function savelink(n,t) // invocata quando si clicca su un link, memorizza quale di questi debba poi essere sostituito. 
258         {
259         if (t=='s') { top.ltr="[?set"+String(n)+"]";}
260         if (t=='v') { top.ltr="[?val"+String(n)+"]";}
261         if (t=='b') { top.ltr="[?bol"+String(n)+"]";}
262 //      alert(ltr);
263         }
264 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. 
265         {
266         pq=query;
267         while (pq.length>0)
268                 {
269                 if (pq.indexOf("[?")>-1)        
270                         {
271                         ltr=pq.slice(pq.indexOf("[?"));
272                         ltr=ltr.substring(ltr.indexOf("[?"),(ltr.length-ltr.indexOf("[?"))-(ltr.length-ltr.indexOf("]")-1));
273                         wto=ltr.substring(2,5);
274                         if (wto=="set") {window.open(top.topurl+action+"set.html","cw");pq="";}
275                         else if (wto=="val") {window.open(top.topurl+action+"val.html","cw");pq="";}
276                         else if (wto=="bol") {window.open(top.topurl+action+"boole.html","cw");pq="";}
277                         else pq=pq.substring(pq.indexOf("[?")+2,pq.length);
278                         }
279                 else {window.open(top.topurl+action+"blank.html","cw");pq="";}
280                 } 
281         }
282 function aggform() // aggiorna il form nel frame centrale. Invocata ad ogni cambio della variabile "query".
283         {
284         cquery=query;
285         while (cquery.indexOf("<")>-1)
286                 {
287                 cquery=cquery.replace(cquery.substring(cquery.indexOf("<"),cquery.indexOf(">")+1),"");
288                 //alert(cquery);
289                 }
290         while (cquery.indexOf("[?")>-1)
291                 {
292                 //alert(cquery);
293                 if (cquery.indexOf("]")>-1)
294                         {
295                         while (cquery.indexOf("]")<cquery.indexOf("[?") && cquery.indexOf("]")>-1)
296                         {cquery=cquery.replace("]","q+u+a+d+r+a+c+h+i+u+s+a");}//alert("loop"+cquery.indexOf("]")+cquery.indexOf("[?"))}
297                         ag1=cquery.slice(cquery.indexOf("[?"));//alert(ag1);
298                         ag1=ag1.substring(ag1.indexOf("[?"),(ag1.length-ag1.indexOf("[?"))-(ag1.length-ag1.indexOf("]")));//alert(ag1);
299                         ag2=ag1.substring(2,5);//alert(ag2);
300                         if (ag2=="set") cquery=cquery.replace(cquery.substring(cquery.indexOf("[?"),cquery.indexOf("]")+1),"<set>");
301                         else if (ag2=="val") cquery=cquery.replace(cquery.substring(cquery.indexOf("[?"),cquery.indexOf("]")+1),"<val>");
302                         else if (ag2=="bol") cquery=cquery.replace(cquery.substring(cquery.indexOf("[?"),cquery.indexOf("]")+1),"<boole>");
303                         else cquery=cquery.replace(cquery.substring(cquery.indexOf("[?"),cquery.indexOf("[?")+1),"q+u+a+d+r+a");
304                         //alert(cquery);
305                         }
306                 else {cquery=cquery.replace("[?","q+u+a+d+r+a?")}
307                 //alert(cquery);        
308                 }
309         while (cquery.indexOf("q+u+a+d+r+a+c+h+i+u+s+a")>-1)
310                 {
311                 cquery=cquery.replace("q+u+a+d+r+a+c+h+i+u+s+a","]");
312                 }
313         while (cquery.indexOf("q+u+a+d+r+a")>-1)
314                 {
315                 cquery=cquery.replace("q+u+a+d+r+a","[");
316                 }
317         while (cquery.indexOf("&lt;")>-1)
318                 {
319                 cquery=cquery.replace("&lt;","<");
320                 }
321         while (cquery.indexOf("&gt;")>-1)
322                 {
323                 cquery=cquery.replace("&gt;",">");
324                 }
325         top.sw.agg();
326         }
327 function ripristina()
328         {
329         //alert (actinput+" "+storia.length);
330         if (numeroazioniannullate>0)
331                 {
332                 numeroazioniannullate--;
333                 query=storia[actinput+1];actinput++;
334                 qw.document.close();
335                 qw.document.write(query);
336                 aggform();
337                 sw.apply();
338                 aggcw();
339                 cw.focus();
340                 }
341         }
342 function annulla()
343         {
344         //alert (actinput+" "+storia.length);
345         if (actinput>0)
346                 {
347                 numeroazioniannullate++;
348                 query=storia[actinput-1];actinput--;
349                 qw.document.close();
350                 qw.document.write(query);
351                 aggform();
352                 sw.apply();
353                 if (query=="*"){cw.location=top.topurl+action+"set.html";ltr="*";} else {aggcw();}
354                 cw.focus();
355                 }
356         }
357 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"
358         {
359         while (fb.indexOf("[set]")>-1){
360         if (fb.indexOf("set")>0)
361                 {
362       fb=fb.replace("[set]","<A HREF="+top.topurl+action+"set.html target=cw onclick=top.savelink("+top.storeps+",'s')>[?set"+top.storeps+"]</A>");
363                 top.storeps++;
364                 }
365                                          }
366         while (fb.indexOf("[val]")>-1){
367         if (fb.indexOf("val")>0)
368                 {
369       fb=fb.replace("[val]","<A HREF="+top.topurl+action+"val.html target=cw onclick=top.savelink("+top.storepv+",'v')>[?val"+top.storepv+"]</A>");
370                 top.storepv++;
371                 }
372                                          }
373         while (fb.indexOf("[boole]")>-1){
374         if (fb.indexOf("boole")>0)
375                 {
376                 fb=fb.replace("[boole]","<A HREF="+top.topurl+action+"boole.html target=cw onclick=top.savelink("+top.storepb+",'b')>[?bol"+top.storepb+"]</A>");
377                 top.storepb++;
378                 }
379                                          }
380         }
381 function aggq() // aggiorna la query sostituendo l' ultimo link editato con la stringa inserita, poi aggiorna tutti i frame.
382         {
383         //window.open(top.topurl+action+"summary.html","cw");
384         qw.document.close();
385         fb=stadd;       
386         nst=ltr.substring(5,(ltr.length-1));// alert(nst+" "+ltr);
387         query=query.replace("<A HREF="+top.topurl+action+"set.html target=cw onclick=top.savelink("+nst+",'s')>"+ltr+"</A>",ltr);
388         query=query.replace("<A HREF="+top.topurl+action+"val.html target=cw onclick=top.savelink("+nst+",'v')>"+ltr+"</A>",ltr);
389         query=query.replace("<A HREF="+top.topurl+action+"boole.html target=cw onclick=top.savelink("+nst+",'b')>"+ltr+"</A>",ltr);
390         parse();
391         query=query.replace(ltr,fb);
392         actinput++;storia[actinput]=query;numeroazioniannullate=0;//alert (actinput+" "+storia.length);
393         qw.document.write(query);aggform();
394         aggcw();
395         cw.focus();
396         }
397 var topurl=document.location.protocol+'//'+document.location.host;
398 //var topurl="";
399 var action="/getpage?url=";
400 //var action="";
401 </SCRIPT>
402 </HEAD>
403   <script>
404     document.write(' <FRAMESET ROWS="69%,31%"> <FRAMESET COLS="40%,60%"> <FRAMESET ROWS="46%,54%"> <FRAME NAME="qw" SRC="'+topurl+action+'start.html"> <FRAME NAME="sw" SRC="'+topurl+action+'blank.html"> </FRAMESET> <FRAME NAME="cw" SRC="'+topurl+action+'blank.html"> </FRAMESET> <FRAMESET COLS="49%,51%"> <FRAME NAME="gw" SRC="'+topurl+action+'blank.html" onFocus="help(-1)";> <FRAME NAME="hw" SRC="'+topurl+action+'blank.html"> </FRAMESET> </FRAMESET>');
405   </script>
406 </HTML>