Bugs fixed:

 1. elim did not accept identifiers with "'" in the middle
 2. elim did not accpet URIs

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 655235c1e538121ca0b72bc124a90bc47db2b139..b7a699c2c993e0f38977d47879273f53117157d2 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -118,7 +118,9 @@ let add_param_substs params =
       params)
 
 let page_RE = Pcre.regexp "&param\\.page=\\d+"
-let identifier_RE = Pcre.regexp "^\\s*\\w+\\s*$"
+let identifier_RE = Pcre.regexp "^\\s*(\\w|')+\\s*$"
+let qualified_mutind_RE =
+ Pcre.regexp "^\\s*cic:(/(\\w|')+)+\\.ind#xpointer\\(1/\\d+\\)\\s*$"
 
 let query_kind_of_req (req: Http_types.request) =
   match req#path with
@@ -233,7 +235,9 @@ let send_results results
 let exec_action dbd (req: Http_types.request) outchan =
   let term_str = req#param "expression" in
   try
-    if req#path = "/elim" && not (Pcre.pmatch ~rex:identifier_RE term_str) then
+    if req#path = "/elim" &&
+     not (Pcre.pmatch ~rex:identifier_RE term_str ||
+          Pcre.pmatch ~rex:qualified_mutind_RE term_str) then
       raise Not_a_MutInd;
     let (context, metasenv) = ([], []) in
     let id_to_uris_raw =