]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/html/expnamedsubst.html
This commit was manufactured by cvs2svn to create branch
[helm.git] / helm / searchEngine / html / expnamedsubst.html
diff --git a/helm/searchEngine/html/expnamedsubst.html b/helm/searchEngine/html/expnamedsubst.html
deleted file mode 100644 (file)
index 3db7aca..0000000
+++ /dev/null
@@ -1,78 +0,0 @@
-<HTML>
-<HEAD>
-<SCRIPT language="Javascript">
-function invia()
-       {
-       stadd="{";
-       for (num=0;num<parent.calias;num++)
-               {
-               stadd=stadd+parent.alist[num]+":=[Expr];";
-               //alert(stadd);
-               }
-       //alert(parent.mcq);
-       //alert(stadd.charAt(stadd.length-1));
-       if (stadd.charAt(stadd.length-1)==";"){stadd=stadd.substring(0,stadd.length-1);}
-       stadd=stadd+"}"
-       if (stadd==("{}")){stadd=""}
-       parent.mcq=parent.mcq.replace("<font color=\"#ff0000\">[exp_named_subst]</font>",stadd);
-       //alert(parent.mcq);
-       //top.qw.document.close();
-       //top.qw.document.write(parent.mcq);
-       parent.parse(parent.mcq);
-       }
-function rimuovialias()
-       {
-       //alert(document.aliaslist.elenco.value);
-       if (document.aliaslist.elenco.value!=""){
-       for (num=Number(document.aliaslist.elenco.value);num<parent.calias;num++)
-               {
-               //alert (parent.alist[num]+" "+parent.alist[num+1]);
-               parent.alist[num]=parent.alist[num+1];
-               }
-       parent.calias--;parent.aggiorna2();}
-       }
-function listalias()
-       {
-       for (num=0;num<parent.calias;num++)
-               {
-               document.write("<OPTION value="+num+">"+parent.alist[num]);
-               //alert (parent.alist[num]);
-               }
-       }
-function addalias()
-       {
-       ok=0;
-       if (document.aliaslist.varid.value.indexOf("/")>0)
-               {if (top.uricheck(document.aliaslist.varid.value)==1 && document.aliaslist.varid.value.substring(document.aliaslist.varid.value.length-3,document.aliaslist.varid.value.length)=="var")
-                       {ok=1}
-               }
-       else {if (top.idcheck(document.aliaslist.varid.value)==1)
-               {ok=1}
-               }       
-       if (ok==1)
-               {
-               //alert (document.aliaslist.idi.value+" "+document.aliaslist.uri.value);
-               parent.alist[parent.calias]=document.aliaslist.varid.value
-               //alert (parent.alist[parent.calias]);
-               parent.calias=parent.calias+1;
-               parent.aggiorna2();
-               }
-       }
-</SCRIPT>
-</HEAD>
-<BODY>
-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.
-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".
-<br>
-<form name="aliaslist" action="Javascript:addalias();" method="get">
-<input name="varid" type=text size="35"> Insert here the Id or the Uri you want to add.
-<input type=submit value="add"><input type=button value="delete selected" onClick="rimuovialias()";>
-<br>
-<select name="elenco" size=7>
-<SCRIPT language=Javascript> listalias(); </SCRIPT>
-</select>
-<br>
-<input type=button value="Done" onClick="invia();" >
-</form>
-</BODY>
-</HTML>