From: Claudio Sacerdoti Coen 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 "¶m\\.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 =