]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/aliaslist.html
snapshot:
[helm.git] / helm / searchEngine / html / aliaslist.html
1 <HTML>
2 <HEAD>
3 <SCRIPT language="Javascript">
4 function invia()
5         {
6         stadd="";
7         for (num=0;num<parent.calias;num++)
8                 {
9                 stadd=stadd+parent.alist[num]+" ";
10                 //alert(stadd);
11                 }
12         //top.window.open(top.topurl+top.action+"editorpdq.html","sw");
13         top.window.sw.editalias(stadd);
14         //alert(parent.mcq);
15         parent.mcq=parent.mcq.replace("<font color=\"#ff0000\">[Alias list]</font>","");
16         //alert(parent.mcq);
17         //top.qw.document.close();
18         //top.qw.document.write(parent.mcq);
19         if (parent.mcq=="<font color=\"#ff0000\">[Alias list]</font> [Expr]")   
20                 {
21                 parent.mcq="[Expr]";
22                 }
23         else 
24                 {
25                 parent.mcq=parent.mcq.replace("<font color=\"#ff0000\">","");
26                 parent.mcq=parent.mcq.replace("</font>","");
27                 }
28         parent.parse(parent.mcq);
29         }
30 function rimuovialias()
31         {
32         //alert(document.aliaslist.elenco.value);
33         if (document.aliaslist.elenco.value!="")
34                 {
35                         for (var i=document.aliaslist.elenco.length-1;i>-1;i--)
36                         {
37                         if (document.aliaslist.elenco.options[i].selected==true)
38                                 {
39                                 for (num=i;num<top.aliasglob.length;num++)
40                                 {
41                                 top.aliasglob[num]=top.aliasglob[num+1];
42                                 }
43                                 top.aliasglob.length--;
44                                 //alert ("rimosso "+i);
45                                 //parent.aggiorna();
46                                 }
47                         }
48                 top.window.open(top.topurl+top.action+"aliaslist.html",(top.cw.frames.length==0?"cw":"bw"));
49                 }
50         }
51 function listalias()
52         {
53         for (num=0;num<top.aliasglob.length;num++)
54                 {
55                 document.write("<OPTION value="+num+">"+top.aliasglob[num]);
56                 //alert (top.aliasglob[num]);
57                 }
58         }
59 function addalias()
60         {
61         if (top.idcheck(document.aliaslist.idi.value)==1 && top.uricheck(document.aliaslist.uri.value)==1)
62                 {
63                 top.aliasglob[top.aliasglob.length]="alias id "+document.aliaslist.idi.value+" = "+document.aliaslist.uri.value;
64                 //parent.aggiorna();
65                 top.window.open(top.topurl+top.action+"aliaslist.html",(top.cw.frames.length==0?"cw":"bw"));
66                 }
67         }
68 function istruzioni()
69         {       
70         top.hw.document.close();
71         top.hw.document.write("You must now enter a list of alias. An Alias is the word 'alias' followed by 'id', an <a href='grammarpdq.html#Id' target='gw'>Id</a>, the equality sign '=', an <a href='grammarpdq.html#Uri' target='gw'>Uri</a>.You may enter as many of them as you want, after each one click the button 'add alias' or press enter and it will be added. When you are done, click 'done'.");
72         }
73 istruzioni();
74 </SCRIPT>
75 </HEAD>
76 <BODY>
77 <form name="aliaslist" action="Javascript:addalias();" method="get">
78 alias id
79 <input name="idi" type=text size="15" value="">
80 =
81 <input name="uri" type=text size="45" value="cic:/"><br>
82 <input type=submit value="add alias"><input type=button value="delete selected" onClick="rimuovialias()";><br>
83 <select name="elenco" multiple size=7>
84 <SCRIPT language=Javascript> listalias(); document.aliaslist.idi.focus(); </SCRIPT>
85 </select>
86 <br>
87 <input type=button value="Done" onClick="top.window.open(top.topurl+top.action+'blank.html','hw');top.window.open(top.topurl+top.action+'editorpdq.html','sw');invia();" ><br>
88 </form>
89 </BODY>
90 </HTML>