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 (top.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 (top.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"><input type=button value="delete selected" onClick="rimuovialias()";>
  70 <br>
  71 <select name="elenco" size=7>
  72 <SCRIPT language=Javascript> listalias(); </SCRIPT>
  73 </select>
  74 <br>
  75 <input type=button value="Done" onClick="invia();" >
  76 </form>
  77 </BODY>
  78 </HTML>