X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=e4e33c629c4f808204dd2b48dcb03057fc6b8240;hb=f15a13bab100064a4da238cede323b8d4568c174;hp=aaa5f48fa34af5210bd8fd43bf2175d684bbdc98;hpb=19802b6487148ac232b560b43f131ffa679e4ee8;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index aaa5f48fa..e4e33c629 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -177,29 +177,9 @@ let contype = "Content-Type", "text/html";;
 
 (* SEARCH ENGINE functions *)
 
-let refine_constraints ((constr_obj:T.r_obj list), (constr_rel:T.r_rel list), (constr_sort:T.r_sort list)) =
- function
-    "/searchPattern" ->
-      U.universe_for_search_pattern,
-       (constr_obj, constr_rel, constr_sort),
-       (Some constr_obj, Some constr_rel, Some constr_sort)
-  | "/matchConclusion" ->
-      let constr_obj' =
-       List.map
-        (function (pos, uri) -> U.set_full_position pos None, uri)
-        (List.filter
-          (function (pos, _) -> U.is_conclusion pos)
-          constr_obj)
-      in
-       U.universe_for_match_conclusion,
-       (*CSC: we must select the must constraints here!!! *)
-       (constr_obj',[],[]),(Some constr_obj', None, None)
-  | _ -> assert false
-;;
-
 let get_constraints term =
  function
-    "/locateInductivePrinciple" ->
+    | "/locateInductivePrinciple" ->
       let uri = 
        match term with
           Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t])
@@ -212,9 +192,19 @@ let get_constraints term =
       let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in
        U.universe_for_search_pattern,
         (constr_obj, constr_rel, constr_sort), (None,None,None)
-  | req_path ->
-     let must = MQueryLevels2.get_constraints term in
-      refine_constraints must req_path
+    | "/searchPattern" ->
+     let constr_obj, constr_rel, constr_sort =
+       CGSearchPattern.get_constraints term in
+      U.universe_for_search_pattern,
+       (constr_obj, constr_rel, constr_sort),
+       (Some constr_obj, Some constr_rel, Some constr_sort)
+    | "/matchConclusion" ->
+     let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in
+(* FG: there is no way to choose the block number ***************************)
+     let block = pred (List.length list_of_must) in 
+      U.universe_for_match_conclusion, 
+      (List.nth list_of_must block, [], []), (Some only, None, None)
+    | _ -> assert false
 ;;
 
 (*
@@ -312,6 +302,14 @@ let callback (req: Http_types.request) outchan =
 	let result = MQueryInterpreter.execute mqi_handle query in
 	      C.close mqi_handle;
         Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
+    | "/unreferred" ->
+        let mqi_handle = C.init mqi_flags debug_print in
+        let target = req#param "target" in
+        let source = req#param "source" in
+	let query = G.unreferred target source in
+	let result = MQueryInterpreter.execute mqi_handle query in
+	      C.close mqi_handle;
+        Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
     | "/getpage" ->
         (* TODO implement "is_permitted" *)
         (let is_permitted _ = true in