X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=35650c8c6cf7e50ab4ee59273bbd60d7496c830a;hb=96134b9ec1030ed15cea00d751dd4d744463f62c;hp=aaa5f48fa34af5210bd8fd43bf2175d684bbdc98;hpb=12dd0be29a6a7dc6ac7a571fa99e2aa728fce4d2;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index aaa5f48fa..35650c8c6 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -213,7 +213,7 @@ let get_constraints term =
        U.universe_for_search_pattern,
         (constr_obj, constr_rel, constr_sort), (None,None,None)
   | req_path ->
-     let must = MQueryLevels2.get_constraints term in
+     let must = CGSearchPattern.get_constraints term in
       refine_constraints must req_path
 ;;
 
@@ -312,6 +312,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