]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/expnamedsubst.html
bb8173389db4c3928a4dbc8d773f5fff428bb0c7
[helm.git] / helm / searchEngine / html / expnamedsubst.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]+":=[Expr];";
10                 //alert(stadd);
11                 }
12         //alert(parent.mcq);
13         //alert(stadd.charAt(stadd.length-1));
14         if (stadd.charAt(stadd.length-1)==";"){stadd=stadd.substring(0,stadd.length-1);}
15         stadd=stadd+"}"
16         if (stadd==("{}")){stadd=""}
17         parent.mcq=parent.mcq.replace("<font color=\"#ff0000\">[exp_named_subst]</font>",stadd);
18         //alert(parent.mcq);
19         //top.qw.document.close();
20         //top.qw.document.write(parent.mcq);
21         parent.parse(parent.mcq);
22         }
23 function rimuovialias()
24         {
25         //alert(document.aliaslist.elenco.value);
26         if (document.aliaslist.elenco.value!=""){
27         for (num=Number(document.aliaslist.elenco.value);num<parent.calias;num++)
28                 {
29                 //alert (parent.alist[num]+" "+parent.alist[num+1]);
30                 parent.alist[num]=parent.alist[num+1];
31                 }
32         parent.calias--;parent.aggiorna2();}
33         }
34 function listalias()
35         {
36         for (num=0;num<parent.calias;num++)
37                 {
38                 document.write("<OPTION value="+num+">"+parent.alist[num]);
39                 //alert (parent.alist[num]);
40                 }
41         }
42 function addalias()
43         {
44         ok=0;
45         if (document.aliaslist.varid.value.indexOf("/")>0)
46                 {if (parent.uricheck(document.aliaslist.varid.value)==1 && document.aliaslist.varid.value.substring(document.aliaslist.varid.value.length-3,document.aliaslist.varid.value.length)=="var")
47                         {ok=1}
48                 }
49         else {if (parent.idcheck(document.aliaslist.varid.value)==1)
50                 {ok=1}
51                 }       
52         if (ok==1)
53                 {
54                 //alert (document.aliaslist.idi.value+" "+document.aliaslist.uri.value);
55                 parent.alist[parent.calias]=document.aliaslist.varid.value
56                 //alert (parent.alist[parent.calias]);
57                 parent.calias=parent.calias+1;
58                 parent.aggiorna2();
59                 }
60         }
61 </SCRIPT>
62 </HEAD>
63 <BODY>
64 You must now enter a list of named_subst. A named_subst is an <a href="grammarpdq.html#Id" target="gw">Id</a> or a <a href="grammarpdq.html#Varuri" target="gw">Varuri</a> followed by ":=" followed by an expression.
65 You may enter as many of them as you want (even none), after each one click the button "add" or press enter and it will be added. When you are done, click "done".
66 <br>
67 <form name="aliaslist" action="Javascript:addalias();" method="get">
68 <input name="varid" type=text size="35"> Insert here the Id or the Uri you want to add.
69 <input type=submit value="add">
70 <input type=button value="Done" onClick="invia();" ><br>
71 <select name="elenco" size=7>
72 <script language=Javascript> listalias(); </script>
73 </select>
74 <br>
75 <input type=button value="delete selected" onClick="rimuovialias()";>
76 </form>
77 </BODY>
78 </HTML>