]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/searchEngine.ml
added CicEnvironment preloading
[helm.git] / helm / searchEngine / searchEngine.ml
index f6e81e2d8aed36998c04503efe15ce7ca7f28052..cef70799e6c1a39c55c88b13f91ec225ccdc26db 100644 (file)
@@ -416,6 +416,18 @@ let callback dbd (req: Http_types.request) outchan =
       let msg = MooglePp.pp_error "Uncaught exception" exn_string in
       send_results (`Error msg) req outchan
 
+let restore_environment () =
+  match
+    Helm_registry.get_opt Helm_registry.get "search_engine.environment_dump"
+  with
+  | None -> ()
+  | Some fname ->
+      printf "Restoring Cic environment from %s ... " fname; flush stdout;
+      let ic = open_in fname in
+      CicEnvironment.restore_from_channel ic;
+      close_in ic;
+      printf "done!\n"; flush stdout
+
 let _ =
   printf "%s started and listening on port %d\n" daemon_name port;
   printf "Current directory is %s\n" (Sys.getcwd ());
@@ -429,6 +441,7 @@ let _ =
       ~user:(Helm_registry.get "db.user")
       ()
   in
+  restore_environment ();
   Http_daemon.start' ~port (callback dbd);
   printf "%s is terminating, bye!\n" daemon_name