]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/editorpdq.html
added Peano module and functions to create natural/real terms
[helm.git] / helm / searchEngine / html / editorpdq.html
1 <HTML>
2 <HEAD>
3 <SCRIPT language="Javascript">
4 var alias="";
5 var expr="";
6 function armageddon()
7         {
8         if (confirm("Are you sure you want to delete your query and start a new one?"))
9                 {
10                 top.terminecic="";top.listaliases="";top.ricordaliaslist=0;top.vlds=new Array();var alias="";var expr="";
11                 top.initialize();
12                 top.window.open(top.topurl+top.action+"start.html","qw");
13                 top.window.open(top.topurl+top.action+"blank.html","cw");
14                 top.window.open(top.topurl+top.action+"blank.html","hw");
15                 top.window.open(top.topurl+top.action+"blank.html","gw");
16                 top.window.open(top.topurl+top.action+"blank.html","sw");
17                 }
18         }
19 function nuovapdqsa()
20         {
21         if (confirm("Are you sure you want to change expression?"))
22                 {
23                 top.terminecic="";
24                 document.invio.expression.value="";document.invio.aliaslist.value=unescape(top.listaliases);
25                 top.ricordaliaslist=1;
26                 window.open(top.topurl+top.action+"pdq.html","cw");
27                 window.open(top.topurl+top.action+"editorpdq.html","sw");
28                 }
29         }
30 function invia()
31         {
32         if (document.invio.expression.value!="")
33                 {top.terminecic=escape(document.invio.expression.value);
34     top.listaliases="";
35                 for (i=0;i<top.aliasglob.length;i++)
36                         {
37                         top.listaliases=top.listaliases+escape(top.aliasglob[i]+" ");
38                         }
39                 //alert(top.listaliases);
40     window.open(top.ask_uwobo(top.topurl+"/"+top.current_query+"?term="+escape(document.invio.expression.value)+"&aliases="+top.listaliases),"cw");
41         }
42                 //window.open(top.topurl+top.action+"templateambigpdq2.html","bw")}     
43         else {alert("Please complete the query before.")}
44         }
45 function warning()
46         {
47         alert("You may not modify this field.",alias);
48         document.invio.aliaslist.value=alias;
49         document.invio.expression.value=expr;
50         }
51 function editalias(valore)
52         {
53         top.window.sw.alias=valore;
54         document.invio.aliaslist.value=valore;
55         }
56 function editexpr(valore)
57         {
58         top.window.sw.expr=valore;
59         document.invio.expression.value=valore;
60         }
61 function listalias()
62         {
63         for (num=0;num<top.aliasglob.length;num++)
64                 {
65                 //alert(top.aliasglob[num]);
66                 document.write("<OPTION value="+num+">"+top.aliasglob[num]);
67                 }
68         }
69 function editaalias()
70         {
71         if (document.invio.expression.value!=""){top.terminecic=escape(document.invio.expression.value)}
72         top.window.open(top.topurl+top.action+"aliaslist.html",(top.cw.frames.length==0?"cw":"bw"));
73         }
74 </SCRIPT>
75 </HEAD>
76 <BODY>
77 <form name="invio" action="Javascript:invia();">
78 <select name="aliaslist" size=1>
79 <SCRIPT language=Javascript> listalias(); </script>
80 </select> Your list of alias.
81 <input type=button value="edit" onMouseOver="top.help(-9)" onClick="editaalias()";>
82 </br>
83 <textarea name="expression" cols="43" rows="6"></textarea><br>Your expression.<br>
84 <input type=submit value="Submit" onMouseOver="top.help(-4)"></input>
85 <input type=button value="Restart" onMouseOver="top.help(-5)" onClick="armageddon()"></input>
86 <input type=button value="New expression" onMouseOver="top.help(-7)" onClick="nuovapdqsa()"></input>
87 </form>
88 <SCRIPT language=Javascript>document.invio.expression.value=unescape(top.terminecic); </script>
89 </BODY>
90 </HTML>