]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/val.html
added Peano module and functions to create natural/real terms
[helm.git] / helm / searchEngine / html / val.html
1 <HTML>
2 <HEAD>
3 <SCRIPT language="Javascript">
4 function listrvars()
5         {
6         for (num=0; num<top.norvars; num++)
7                 {
8                 document.write("<OPTION value="+top.rvars[num]+">"+top.rvars[num]);
9                 }
10         }
11 function listvvars1()
12         {
13         for (num=0; num<top.novvars1; num++)
14                 {
15                 document.write("<OPTION value="+top.vvars1[num]+">"+top.vvars1[num]);
16                 }
17         }
18 function listvvars2()
19         {
20         for (num=0; num<top.novvars2; num++)
21                 {
22                 document.write("<OPTION value="+top.vvars2[num]+">"+top.vvars2[num]);
23                 }
24         }
25 function help()
26         {
27         with (document.form1) {
28         if (selopt[0].checked)
29         alert ("No help available.");
30         if (selopt[1].checked)
31         alert ("Turns a list of strings which can have attributes ( the [set] ) in a list of strings which cannot have them ( a [val] ).");
32         if (selopt[2].checked)
33         alert ("Returns the attribute of the given [vvar] in the given [rvar].");
34         if (selopt[3].checked)
35         alert ("No help available.");
36         if (selopt[4].checked)
37         alert ("Parenthesis are employed to force precedence between operators.");
38         if (selopt[5].checked)
39         alert ("The [path] you must enter represents a relation; this production returns a [val] composed by the union of all the URIs which match the chosen relation in the [val] you will enter afterwards. If you select 'inverse', you'll obtain a list of all the URIs for which the [val] matches the chosen relation, 'sub' and 'super' modify the result depending on the chosen relation.");
40         }
41         }
42 function choice()
43 {
44 top.stadd="";top.wrong=0;voidfield=1;
45 with (document.form1) {
46         if (selopt[0].checked) {
47                 voidfield=0;
48                 val1.value=top.tpa(val1.value);
49                 top.stadd=val1.value;
50                 top.gramcheck("qsl",val1.value);
51                                           }
52         if (selopt[1].checked) {
53                 top.stadd="refof [set]";
54                                           }
55         if (selopt[2].checked) {
56                 if (val2.value==""||val8.value==""){voidfield=1;}
57                 else {top.stadd=val2.value+"."+val8.value;}
58                                           }
59         if (selopt[3].checked) {
60                 top.stadd=val3.value;
61                                           }
62         if (selopt[4].checked) {
63                 top.stadd="([val])";
64                                           }
65         if (selopt[5].checked) {
66                 voidfield=0;
67                 val6.value=top.tpa(val6.value);
68                 top.stadd="property "+val45.value+" "+val5.value+" "+val6.value+" [val]";
69                 top.gramcheck("qp",val6.value);
70                                           }
71         if (selopt[6].checked) {
72                 val7.value=top.tpa(val7.value);
73                 top.stadd=val7.value;
74                 if (val7.value!="") {inputok=1} else voidfield=1;
75                                           }
76                    }
77 if (top.stadd!="") top.aggq();
78         else if (voidfield==1) alert ("You left at least one field unfilled");
79 }
80 </SCRIPT>
81 </HEAD>
82 <BODY>
83 <h1> <SCRIPT language="Javascript">document.write(top.ltr) </SCRIPT>
84 <input type="button" value="&lt;-" onmouseOver="top.help(-8)" onclick="top.annulla()">
85 <input type="button" value="-&gt;" onmouseOver="top.help(-81)" onclick="top.ripristina()"></h1>
86 <h2> Select one of the following: </h2>
87 <form name="form1" action="Javascript:choice();" method="get">
88 <input type="radio" name="selopt"> <input name="val1" type=text value="{&quot;&quot;}" onFocus="selopt[0].checked=true;top.help(7)"> <br>
89 <input type="radio" name="selopt"> refof [set] <br>
90 <input type="radio" name="selopt"> <select name="val2" type=text onFocus="selopt[2].checked=true;top.help(4)">
91 <SCRIPT language=Javascript> listrvars(); </SCRIPT>
92 </select> . <select name="val8" type=text onFocus="selopt[2].checked=true;top.help(8)">
93 <SCRIPT language=Javascript> listvvars2(); </SCRIPT>
94 </select>
95 <br>
96 <input type="radio" name="selopt"> <select name="val3" type=text onFocus="selopt[3].checked=true;top.help(81)">
97 <SCRIPT language=Javascript> listvvars1(); </SCRIPT>
98 </select>
99 <br>
100 <input type="radio" name="selopt"> ( [val] ) <br>
101 <input type="radio" name="selopt"> property
102 <select name="val45" onFocus="selopt[5].checked=true">
103 <OPTION selected value="">  
104 <OPTION value=inverse> inverse
105 </select> 
106 <select name="val5" onFocus="selopt[5].checked=true">
107 <OPTION selected value=""> 
108 <OPTION value=sub> sub
109 <OPTION value=super> super
110 </select> <input name="val6" type=text value="&quot;&quot;" onFocus="selopt[5].checked=true;top.help(5)"> [val] <br>
111 <input type="radio" name="selopt"> <input name="val7" type=text onFocus="selopt[6].checked=true;top.help(1)">  <br>
112 <input type="submit" value="compose"><input type="button" value="get help" onclick="help()">
113 </form>
114 </BODY>
115 </HTML>