]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/aliaslist.html
Many changes in the client-side interfaces:
[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                 for (num=Number(document.aliaslist.elenco.value);num<top.aliasglob.length;num++)
35                 {
36                 top.aliasglob[num]=top.aliasglob[num+1];
37                 }
38                 top.aliasglob.length--;
39                 //parent.aggiorna();
40                 top.window.open(top.topurl+top.action+"aliaslist.html",(top.cw.frames.length==0?"cw":"bw"));
41         }
42         }
43 function listalias()
44         {
45         for (num=0;num<top.aliasglob.length;num++)
46                 {
47                 document.write("<OPTION value="+num+">"+top.aliasglob[num]);
48                 //alert (top.aliasglob[num]);
49                 }
50         }
51 function addalias()
52         {
53         if (top.idcheck(document.aliaslist.idi.value)==1 && top.uricheck(document.aliaslist.uri.value)==1)
54                 {
55                 top.aliasglob[top.aliasglob.length]="alias "+document.aliaslist.idi.value+" "+document.aliaslist.uri.value;
56                 //parent.aggiorna();
57                 top.window.open(top.topurl+top.action+"aliaslist.html",(top.cw.frames.length==0?"cw":"bw"));
58                 }
59         }
60 function istruzioni()
61         {       
62         top.hw.document.close();
63         top.hw.document.write("You must now enter a list of alias. An Alias is the word 'alias' followed by an <a href='grammarpdq.html#Id' target='gw'>Id</a>, followed by 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'.");
64         }
65 istruzioni();
66 </SCRIPT>
67 </HEAD>
68 <BODY>
69 <form name="aliaslist" action="Javascript:addalias();" method="get">
70 alias
71 <input name="idi" type=text size="15">
72 <input name="uri" type=text size="45" value="cic:/"><br>
73 <input type=submit value="add alias"><input type=button value="delete selected" onClick="rimuovialias()";><br>
74 <select name="elenco" size=7>
75 <script language=Javascript> listalias(); document.aliaslist.idi.focus(); </script>
76 </select>
77 <br>
78 <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>
79 </form>
80 </BODY>
81 </HTML>