exception Not_a_MutInd
let daemon_name = "Whelp"
-let configuration_file = "/projects/helm/etc/whelp.conf.xml"
+let configuration_file = "searchEngine.conf.xml"
let placeholders = [
"ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
moogle_TPL
let exec_action dbd (req: Http_types.request) outchan =
+ let dbd = dbd () in
let term_str = req#param "expression" in
try
if req#path = "/elim" &&
end
in
let module Disambiguate' = Disambiguate.Make(Chat) in
-prerr_endline "VOVI";
- let ast = Grammar.Entry.parse CicNotationParser.term (Stream.of_string term_str) in
-prerr_endline "VIVO";
+ let ast =
+ CicNotationParser.parse_term (Ulexing.from_utf8_string term_str) in
let (id_to_uris, metasenv, term) =
match
Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
| "/match" -> Whelp.match_term ~dbd term
| "/instance" -> Whelp.instance ~dbd term
| "/hint" ->
- let status = ProofEngineTypes.initial_status term metasenv in
+ let status = ProofEngineTypes.initial_status term metasenv [] in
let intros = PrimitiveTactics.intros_tac () in
let subgoals = ProofEngineTypes.apply_tactic intros status in
(match subgoals with
^ " type")))
req outchan
-let callback (dbd, (req: Http_types.request), outchan) =
+let callback dbd (req: Http_types.request) outchan =
try
debug_print (sprintf "Received request: %s" req#path);
(match req#path with
if expression = "" then
send_results (`Results []) req outchan
else begin
- let results = Whelp.locate ~dbd expression in
+ let results = Whelp.locate ~dbd:(dbd ()) expression in
let results = List.map UriManager.string_of_uri results in
send_results (`Results results) req outchan
end
let msg = MooglePp.pp_error "Uncaught exception" exn_string in
send_results (`Error msg) req outchan
-let callback dbd req ch =
- HExtlib.finally
- (fun () -> try close_out ch with Sys_error _ -> ())
- callback (dbd, req, ch)
-
let restore_environment () =
match
Helm_registry.get_opt Helm_registry.string "search_engine.environment_dump"
printf "done!\n"; flush stdout
let read_notation () =
- CicNotation2.load_notation ~include_paths:[]
- (Helm_registry.get "search_engine.notations");
- CicNotation2.load_notation ~include_paths:[]
- (Helm_registry.get "search_engine.interpretations")
+ ignore (CicNotation2.load_notation ~include_paths:[]
+ (Helm_registry.get "search_engine.notations"));
+ ignore (CicNotation2.load_notation ~include_paths:[]
+ (Helm_registry.get "search_engine.interpretations"))
let _ =
printf "%s started and listening on port %d\n" daemon_name port;
printf "HTML directory is %s\n" pages_dir;
flush stdout;
Unix.putenv "http_proxy" "";
- let dbd =
- HMysql.quick_connect
- ~host:(Helm_registry.get "db.host")
- ~database:(Helm_registry.get "db.database")
- ~user:(Helm_registry.get "db.user")
- ()
+ let dbd () =
+ let dbd = LibraryDb.instance () in
+ MetadataTypes.ownerize_tables "searchEngine";
+ LibraryDb.create_owner_environment ();
+ dbd
in
restore_environment ();
read_notation ();
- let d_spec = Http_daemon.daemon_spec ~port ~callback:(callback dbd) () in
+ let d_spec = Http_daemon.daemon_spec ~port ~callback:(callback dbd) ~auto_close:true () in
Http_daemon.main d_spec;
printf "%s is terminating, bye!\n" daemon_name