From: Stefano Zacchiroli Date: Thu, 26 Dec 2002 19:57:13 +0000 (+0000) Subject: catch CTRL-C and save maps before quitting X-Git-Tag: v0_3_99~112 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a96d06ae093236a3be8461912926903e81751578;p=helm.git catch CTRL-C and save maps before quitting --- diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index 0644fcc7d..7eb8deae4 100644 --- a/helm/http_getter/http_getter.ml +++ b/helm/http_getter/http_getter.ml @@ -83,6 +83,7 @@ let xml_map = new Http_getter_map.map Http_getter_env.xml_dbm in let rdf_map = new Http_getter_map.map Http_getter_env.rdf_dbm in let xsl_map = new Http_getter_map.map Http_getter_env.xsl_dbm in +let save_maps () = xml_map#close; rdf_map#close; xsl_map#close in let map_of_uri = function | uri when is_xml_uri uri -> xml_map | uri when is_rdf_uri uri -> rdf_map @@ -361,7 +362,8 @@ let callback (req: Http_types.request) outchan = | "/getempty" -> Http_daemon.respond ~body:Http_getter_const.empty_xml outchan | invalid_request -> - Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan) + Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); + debug_print "Done!" with | Http_types.Param_not_found attr_name -> return_400 (sprintf "Parameter '%s' is missing" attr_name) outchan @@ -377,6 +379,10 @@ in Http_getter_env.dump_env (); flush stdout; Unix.putenv "http_proxy" ""; -Http_daemon.start' - ~timeout:None ~port:Http_getter_env.port ~mode:`Thread callback +Sys.catch_break true; +try + Http_daemon.start' + ~timeout:None ~port:Http_getter_env.port ~mode:`Thread callback +with Sys.Break -> + save_maps ()