]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/searchEngine.ml
- new generated query "unreferred" implemented at server side
[helm.git] / helm / searchEngine / searchEngine.ml
index aaa5f48fa34af5210bd8fd43bf2175d684bbdc98..35650c8c6cf7e50ab4ee59273bbd60d7496c830a 100644 (file)
@@ -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