From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 26 May 2005 13:10:32 +0000 (+0000)
Subject: Bugs fixed:
X-Git-Tag: PRE_INDEX_1~120
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=403c0a86bc67e674e5dc4a7ff822180d761a5159;p=helm.git

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 655235c1e..b7a699c2c 100644
--- 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 =