X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=afb274f460e07f008d746d2fee0be5ac3f8182c0;hb=93242489b31efb28345fbcf3ff6f319d9b487c0e;hp=7c5c6e36e7ab916c7635dd941fa2c878c83b6a06;hpb=d34100cdde334a8e93876d190b8a11aba4003a91;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 7c5c6e36e..afb274f46 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -43,7 +43,7 @@ let placeholders = [
   "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
   "EXPRESSION"; "ID"; "IDEN"; "ID_TO_URIS"; "INTERPRETATIONS";
   "INTERPRETATIONS_LABELS"; "MSG"; "NEW_ALIASES"; "NEXT_LINK"; "NO_CHOICES";
-  "PAGE"; "PAGES"; "PREV_LINK"; "QUERY_KIND"; "QUERY_SUMMARY"; "RESULTS";
+  "PAGE"; "PAGES"; "PAGELIST"; "PREV_LINK"; "QUERY_KIND"; "QUERY_SUMMARY"; "RESULTS";
   "SEARCH_ENGINE_URL"; "SIMPLE_CHECKED"; "TITLE";
 ]
 
@@ -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
@@ -126,6 +128,7 @@ let query_kind_of_req (req: Http_types.request) =
   | "/hint" -> "Hint"
   | "/locate" -> "Locate"
   | "/elim" -> "Elim"
+  | "/instance" -> "Instance"
   | _ -> ""
 
   (* given a uri with a query part in input try to find in it a string
@@ -142,6 +145,14 @@ let patch_param param_name param_value url =
   (** HTML encoding, e.g.: "<" -> "&lt;" *)
 let html_encode = Netencoding.Html.encode_from_latin1
 
+let fold_n_to_m f n m acc =
+ let rec aux acc =
+  function
+     i when i <= m -> aux (f i acc) (i + 1)
+   | _ -> acc
+ in
+  aux acc n
+
 let send_results results
   ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") 
    (req: Http_types.request) outchan
@@ -178,9 +189,28 @@ let send_results results
             results_no / results_per_page + 1
         in
         let pages = if pages = 0 then 1 else pages in
+        let additional_pages = 3 in
         let (summary, results) = MooglePp.theory_of_result page results in
         [ tag "PAGE", string_of_int page;
-          tag "PAGES", string_of_int pages;
+          tag "PAGES", string_of_int pages ^ " Pages";
+          tag "PAGELIST",
+          (let inf = page - additional_pages in
+           let sup = page + additional_pages in
+           let superinf = inf - (sup - pages) in
+           let supersup = sup + (1 - inf) in
+           let n,m =
+            if inf >= 1 && sup <= pages then
+             inf,sup
+            else if inf < 1 then
+             1, (if supersup <= pages then supersup else pages)
+            else (* sup > pages *)
+             (if superinf >= 1 then superinf else 1),pages
+           in
+            fold_n_to_m
+             (fun n acc -> acc ^ " " ^
+                          (if n = page then string_of_int n
+                           else page_link (string_of_int n) n))
+             n m "");
           tag "PREV_LINK", (if page > 1 then page_link "Prev" (page-1) else "");
           tag "NEXT_LINK",
             (if page < pages then page_link "Next" (page+1) else "");
@@ -189,7 +219,8 @@ let send_results results
           tag "RESULTS", results ]
     | `Error msg ->
         [ tag "PAGE", "1";
-          tag "PAGES", "1";
+          tag "PAGES", "1 Page";
+          tag "PAGELIST", "";
           tag "PREV_LINK", "";
           tag "NEXT_LINK", "";
           tag "QUERY_KIND", query_kind;
@@ -232,7 +263,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 = 
@@ -332,6 +365,7 @@ let exec_action dbd (req: Http_types.request) outchan =
     let uris =
       match req#path with
       | "/match" -> MetadataQuery.match_term ~dbd term
+      | "/instance" -> MetadataQuery.instance ~dbd term
       | "/hint" ->
           let status = ProofEngineTypes.initial_status term metasenv in
           let intros = PrimitiveTactics.intros_tac () in
@@ -339,7 +373,7 @@ let exec_action dbd (req: Http_types.request) outchan =
           (match subgoals with
           | proof, [goal] ->
               let (uri,metasenv,bo,ty) = proof in
-              List.map fst (MetadataQuery.hint ~dbd (proof, goal))
+              List.map fst (MetadataQuery.experimental_hint ~dbd (proof, goal))
           | _ -> assert false)
       | "/elim" ->
           let uri =
@@ -410,6 +444,7 @@ let callback dbd (req: Http_types.request) outchan =
         end
     | "/hint"
     | "/elim"
+    | "/instance"
     | "/match" -> exec_action dbd req outchan
     | invalid_request ->
         Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))