]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/searchEngine.ml
mathql interpreter flags can be now red from helm registry
[helm.git] / helm / searchEngine / searchEngine.ml
index d79e6ebd4cd757c2028c1f8fb796f69b661cc68b..507dadb63d207546cd9cee1cabe272c315aab669 100644 (file)
@@ -35,8 +35,6 @@ let debug_print s = if debug then prerr_endline s;;
 Http_common.debug := true;;
 (* Http_common.debug := true;; *)
 
-let mqi_flags = [] (* default MathQL interpreter options *)
-
 open Printf;;
 
 let daemon_name = "Search Engine";;
@@ -264,33 +262,27 @@ in
 
 (* HTTP DAEMON CALLBACK *)
 
-let callback (req: Http_types.request) outchan =
+let callback mqi_handle (req: Http_types.request) outchan =
   try
     debug_print (sprintf "Received request: %s" req#path);
     (match req#path with
     | "/execute" ->
-        let mqi_handle = C.init mqi_flags debug_print in 
         let query_string = req#param "query" in
         let lexbuf = Lexing.from_string query_string in
         let query = MQueryUtil.query_of_text lexbuf in
         let result = MQueryInterpreter.execute mqi_handle query in
         let result_string = pp_result result in
-             C.close mqi_handle;
         Http_daemon.respond ~body:result_string ~headers:[contype] outchan
     | "/locate" ->
-        let mqi_handle = C.init mqi_flags debug_print in
         let id = req#param "id" in
         let query = G.locate id in
         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" *)
@@ -347,7 +339,6 @@ let callback (req: Http_types.request) outchan =
     | "/searchPattern"
     | "/matchConclusion"
     | "/locateInductivePrinciple" ->
-        let mqi_handle = C.init mqi_flags debug_print in
         let term_string = req#param "term" in
         let (context, metasenv) = ([], []) in
         let id_to_uris_raw = req#param "aliases" in
@@ -601,8 +592,7 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
             Http_daemon.respond
               ~headers:[contype]
               ~body:"some implicit variables are still unistantiated :-("
-              outchan);
-            C.close mqi_handle
+              outchan)
     | invalid_request ->
         Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
     debug_print (sprintf "%s done!" req#path)
@@ -620,6 +610,7 @@ printf "Current directory is %s\n" (Sys.getcwd ());
 printf "HTML directory is %s\n" pages_dir;
 flush stdout;
 Unix.putenv "http_proxy" "";
-Http_daemon.start' ~port callback;
+let mqi_handle = C.init debug_print in
+Http_daemon.start' ~port (callback mqi_handle);
+C.close mqi_handle;
 printf "%s is terminating, bye!\n" daemon_name
-