]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/aliaslist.html
- the mathql interpreter is not helm-dependent any more
[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 "+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 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'.");
72         }
73 istruzioni();
74 </SCRIPT>
75 </HEAD>
76 <BODY>
77 <form name="aliaslist" action="Javascript:addalias();" method="get">
78 alias
79 <input name="idi" type=text size="15" value="">
80 <input name="uri" type=text size="45" value="cic:/"><br>
81 <input type=submit value="add alias"><input type=button value="delete selected" onClick="rimuovialias()";><br>
82 <select name="elenco" multiple size=7>
83 <SCRIPT language=Javascript> listalias(); document.aliaslist.idi.focus(); </SCRIPT>
84 </select>
85 <br>
86 <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>
87 </form>
88 </BODY>
89 </HTML>