]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/html/expr.html
Many changes in the client-side interfaces:
[helm.git] / helm / searchEngine / html / expr.html
index 291b40cc287983c85c4a6d0b43cfadc3fd7c1a9e..bc34e72fed6a713bbf3f7fd7981ffc2f7622f9e1 100644 (file)
@@ -21,9 +21,16 @@ with (document.form1) {
                                {stadd=stadd+"[Expr] "}
                                stadd=stadd+")";
                               }
-       parent.mcq=parent.mcq.replace("<font color=\"#ff0000\">[Expr]</font>",stadd);
+       if (selopt[6].checked) {
+                               stadd=document.form1.id_or_uri.value;
+                               //alert(stadd.substring(0,5));
+                               if (stadd.substring(0,5)=="cic:/") 
+                                       {if (!parent.uricheck(stadd)){stadd="";}}
+                               else if (!parent.idcheck(stadd)){stadd="";}                                     
+                               }
+       if (stadd!="") {parent.mcq=parent.mcq.replace("<font color=\"#ff0000\">[Expr]</font>",stadd);
        //top.qw.document.write(parent.mcq);
-       parent.parse(parent.mcq);
+       parent.parse(parent.mcq);}
                        }
        }
 </SCRIPT>
@@ -45,6 +52,7 @@ You are entering an expression. Select one of the following.
 <option value="?"> ?
 </select> <br>
 <input type="radio" name="selopt"> ( [Expr list] ) <br>
+<input type="radio" name="selopt"> <input name="id_or_uri" type="text" onFocus="selopt[6].checked=true;top.help(-10)"><br>
 <input type=submit value="Select">
 </form>
 </BODY>