From 6857e22b8a58162893119f7747c5848031fd59ce Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 5 Jul 2005 08:11:00 +0000 Subject: [PATCH] ported to new getter interface --- helm/matita/.depend | 50 ++++++------- helm/matita/Makefile.in | 3 - helm/matita/matita.conf.xml.sample | 14 ++-- helm/matita/matita.ml | 12 +--- helm/matita/matitaDb.ml | 6 +- helm/matita/matitaEngine.ml | 8 +-- helm/matita/matitaExcPp.ml | 13 ++-- helm/matita/matitaMathView.ml | 70 ++++++++++--------- helm/matita/matitaMathView.mli | 2 - helm/matita/matitaSync.ml | 35 +++------- helm/matita/matitaSync.mli | 1 - helm/matita/matitacLib.ml | 7 +- helm/matita/matitaclean.ml | 9 +-- helm/matita/updater.ml | 10 --- helm/ocaml/cic/cicParser.ml | 13 +++- helm/ocaml/cic/test.ml | 4 +- .../cic_proof_checking/cicEnvironment.ml | 41 ++--------- .../metadata/extractor/extractor_manager.ml | 1 - 18 files changed, 117 insertions(+), 182 deletions(-) delete mode 100644 helm/matita/updater.ml diff --git a/helm/matita/.depend b/helm/matita/.depend index d85173458..d6272980d 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,11 +1,19 @@ -matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi matitaDisambiguator.cmi buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx matitaDisambiguator.cmx buildTimeConf.cmx +matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \ + matitacleanLib.cmi +matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \ + matitacleanLib.cmi +matitaclean.cmo: matitacleanLib.cmi matitaDb.cmi +matitaclean.cmx: matitacleanLib.cmx matitaDb.cmx +matitacLib.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi \ + matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx \ + matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi +matitac.cmo: matitacLib.cmi +matitac.cmx: matitacLib.cmx matitaDb.cmo: matitaMisc.cmi matitaDb.cmi matitaDb.cmx: matitaMisc.cmx matitaDb.cmi +matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi +matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaEngine.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ @@ -34,30 +42,24 @@ matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmi matitaMisc.cmo: matitaTypes.cmo buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi -matitaScript.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ - matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi matitaScript.cmi -matitaScript.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \ - matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx matitaScript.cmi +matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi matitaDisambiguator.cmi buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx matitaDisambiguator.cmx buildTimeConf.cmx +matitaScript.cmo: matitacleanLib.cmi matitaTypes.cmo matitaSync.cmi \ + matitaMisc.cmi matitaLog.cmi matitaEngine.cmi matitaDisambiguator.cmi \ + matitaDb.cmi matitaScript.cmi +matitaScript.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \ + matitaMisc.cmx matitaLog.cmx matitaEngine.cmx matitaDisambiguator.cmx \ + matitaDb.cmx matitaScript.cmi matitaSync.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ matitaSync.cmi matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ matitaSync.cmi matitaTypes.cmo: matitaLog.cmi matitaTypes.cmx: matitaLog.cmx -matitac.cmo: matitacLib.cmi -matitac.cmx: matitacLib.cmx -matitacLib.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi \ - matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx \ - matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi -matitaclean.cmo: matitacleanLib.cmi matitaDb.cmi -matitaclean.cmx: matitacleanLib.cmx matitaDb.cmx -matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \ - matitacleanLib.cmi -matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \ - matitacleanLib.cmi -matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi -matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx matitaDisambiguator.cmi: matitaTypes.cmo matitaEngine.cmi: matitaTypes.cmo matitaGtkMisc.cmi: matitaGeneratedGui.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index d1eff032a..4d03f8dfc 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -54,9 +54,6 @@ CLEANCMOS = $(CCMOS) matitacleanLib.cmo all: matita matitac matitatop cicbrowser matitadep matitaclean -updater: $(LIB_DEPS) - $(OCAMLC) $(PKGS) -linkpkg -o $@ updater.ml - ifeq ($(HAVE_OCAMLOPT),yes) CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index c68c57fa9..56a04d605 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -16,13 +16,15 @@ matita
- - @@PREFETCH@@ - - file:///projects/helm/library/coq_contribs - .matita/getter/cache - .matita/getter/maps /projects/helm/xml/dtd + + cic:/ + file:///projects/helm/library/coq_contribs/ + + + cic:/matita/ + .matita/xml/matita/ +
diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 3eb0fc6a1..251f72017 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -148,12 +148,6 @@ let _ = (MatitaMathView.sequentViewer_instance ())#get_selected_terms); addDebugItem "dump getter settings" (fun _ -> prerr_endline (Http_getter_env.env_to_string ())); - addDebugItem "getter: update" - (fun _ -> - ignore (Thread.create (fun () -> - MatitaLog.message "Rebuilding getter maps in background ..."; - Http_getter.update (); - MatitaLog.message "Getter maps successfully rebuilt.") ())); addDebugItem "getter: getalluris" (fun _ -> List.iter prerr_endline (Http_getter.getalluris ())); addDebugItem "dump script status" script#dump; @@ -184,11 +178,7 @@ let _ = (** *) let _ = - at_exit - (fun () -> - Http_getter_logger.log "Sync map tree to disk..."; - Http_getter.sync_dump_file (); - print_endline "\nThanks for using Matita!\n"); + at_exit (fun () -> print_endline "\nThanks for using Matita!\n"); Sys.catch_break true; (try gui#loadScript Sys.argv.(1); diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml index b8f91a342..089aab157 100644 --- a/helm/matita/matitaDb.ml +++ b/helm/matita/matitaDb.ml @@ -37,6 +37,7 @@ let instance = let xpointer_RE = Pcre.regexp "#.*$" +let file_scheme_RE = Pcre.regexp "^file://" let clean_owner_environment () = let dbd = instance () in @@ -65,10 +66,7 @@ let clean_owner_environment () = (fun uri -> let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in List.iter - (fun suffix -> - (*prerr_endline ("unregistering " ^ uri ^ suffix);*) - Http_getter.unregister (uri ^ suffix)) - + (fun suffix -> Http_getter_storage.remove (uri ^ suffix ^ ".xml.gz")) [""; ".body"; ".types"]) owned_uris; List.iter (fun statement -> diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index cb420d267..5919a7bfc 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -132,18 +132,14 @@ let eval_coercion status coercion = match coercion with | Cic.Const (uri,_) | Cic.Var (uri,_) -> - let o,_ = - CicEnvironment.get_obj CicUniv.empty_ugraph uri - in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in (match o with | Cic.Constant (_,_,ty,_,_) | Cic.Variable (_,_,ty,_,_) -> uri,ty | _ -> assert false) | Cic.MutConstruct (uri,t,c,_) -> - let o,_ = - CicEnvironment.get_obj CicUniv.empty_ugraph uri - in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in (match o with | Cic.InductiveDefinition (l,_,_,_) -> let (_,_,_,cl) = List.nth l t in diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index c672e2e70..74f2c9f41 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -23,14 +23,19 @@ * http://helm.cs.unibo.it/ *) -open MatitaTypes;; -open Printf;; +open Printf let to_string = function - | Option_error ("baseuri", "not found" ) -> - "Baseuri not set for this script. Use 'set \"baseuri\" \"\".' to set it." + | MatitaTypes.Option_error ("baseuri", "not found" ) -> + "Baseuri not set for this script. " + ^ "Use 'set \"baseuri\" \"\".' to set it." + | MatitaTypes.Command_error msg -> "Error: " ^ msg | CicTextualParser2.Parse_error (floc,err) -> let (x, y) = CicAst.loc_of_floc floc in sprintf "Parse error at %d-%d: %s" x y err + | UriManager.IllFormedUri uri -> sprintf "invalid uri: %s" uri + | CicEnvironment.Object_not_found uri -> + sprintf "object not found: %s" (UriManager.string_of_uri uri) | exn -> "Uncaught exception: " ^ Printexc.to_string exn + diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 2151541a3..cd600f040 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -300,8 +300,6 @@ type term_source = | `String of string ] -exception Browser_failure of string - class type cicBrowser = object method load: MatitaTypes.mathViewer_entry -> unit @@ -309,6 +307,12 @@ object method loadInput: string -> unit end +let reloadable = function + | `About `Current_proof + | `Dir _ -> + true + | _ -> false + class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) () = @@ -316,9 +320,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let whelp_RE = Pcre.regexp "^\\s*whelp" in let uri_RE = Pcre.regexp - "^cic:/(\\w+/)*\\w+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$" + "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$" in - let dir_RE = Pcre.regexp "^cic:((/(\\w+/)*\\w+(/)?)|/|)$" in + let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in let trailing_slash_RE = Pcre.regexp "/$" in let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in @@ -361,8 +365,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let handle_error f = try f () - with exn -> - fail (MatitaExcPp.to_string exn) + with exn -> fail (MatitaExcPp.to_string exn) in let handle_error' f = (fun () -> handle_error (fun () -> f ())) in object (self) @@ -404,9 +407,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) GMain.quit (); false)); ignore(win#whelpResultTreeview#connect#row_activated - ~callback:(fun _ _ -> self#loadInput (self#_getSelectedUri ()))); + ~callback:(fun _ _ -> + handle_error (fun () -> self#loadInput (self#_getSelectedUri ())))); mathView#set_href_callback (Some (fun uri -> - handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri))))); + handle_error (fun () -> + self#load (`Uri (UriManager.uri_of_string uri))))); self#_load (`About `Blank); toplevel#show () @@ -417,10 +422,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) val model = new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview + val mutable lastDir = "" (* last loaded "directory" *) + method private _getSelectedUri () = match model#easy_selection () with | [sel] when is_uri sel -> sel (* absolute URI selected *) - | [sel] -> win#browserUri#entry#text ^ sel (* relative URI selected *) +(* | [sel] -> win#browserUri#entry#text ^ sel |+ relative URI selected +| *) + | [sel] -> lastDir ^ sel | _ -> assert false (** history RATIONALE @@ -467,25 +475,22 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) * @param uri string *) method private _load entry = try - if entry <> current_entry || entry = `About `Current_proof then begin - (match entry with - | `About `Current_proof -> self#home () - | `About `Blank -> self#blank () - | `About `Us -> () (* TODO implement easter egg here :-] *) - | `Check term -> self#_loadCheck term - | `Cic (term, metasenv) -> self#_loadTermCic term metasenv - | `Dir dir -> self#_loadDir dir - | `Uri uri -> self#_loadUriManagerUri uri - | `Whelp (query, results) -> - set_whelp_query query; - self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) results)); - self#setEntry entry - end - with - | UriManager.IllFormedUri uri -> fail (sprintf "invalid uri: %s" uri) - | CicEnvironment.Object_not_found uri -> - fail (sprintf "object not found: %s" (UriManager.string_of_uri uri)) - | Browser_failure msg -> fail msg + if entry <> current_entry || reloadable entry then begin + (match entry with + | `About `Current_proof -> self#home () + | `About `Blank -> self#blank () + | `About `Us -> () (* TODO implement easter egg here :-] *) + | `Check term -> self#_loadCheck term + | `Cic (term, metasenv) -> self#_loadTermCic term metasenv + | `Dir dir -> self#_loadDir dir + | `Uri uri -> self#_loadUriManagerUri uri + | `Whelp (query, results) -> + set_whelp_query query; + self#_loadList (List.map (fun r -> "obj", + UriManager.string_of_uri r) results)); + self#setEntry entry + end + with exn -> fail (MatitaExcPp.to_string exn) method private blank () = self#_showMath; @@ -524,7 +529,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri) content in - if l = [] then raise (Browser_failure "no such directory"); + lastDir <- dir; self#_loadList l method private setEntry entry = @@ -588,7 +593,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (try entry_of_string txt with Invalid_argument _ -> - raise (Browser_failure (sprintf "unsupported uri: %s" txt))) + command_error (sprintf "unsupported uri: %s" txt)) in self#_load entry; self#_historyAdd entry @@ -604,10 +609,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method history = history method currentEntry = current_entry method refresh () = - if current_entry = `About `Current_proof then - self#_load (`About `Current_proof) - end + if reloadable current_entry then self#_load current_entry + end let sequentsViewer ~(notebook:GPack.notebook) ~(sequentViewer:sequentViewer) () diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index ed57b886c..045555b80 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -59,8 +59,6 @@ class type sequentsViewer = method goto_sequent: int -> unit (* to be called _after_ load_sequents *) end -exception Browser_failure of string - class type cicBrowser = object method load: MatitaTypes.mathViewer_entry -> unit diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 8f8a66e09..374b47870 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -123,12 +123,9 @@ let save_object_to_disk status uri obj = (List.map Filename.dirname [innertypespath; xmlpath]); (* now write to disk *) ensure_path_exists innertypespath; - Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ; + Xml.pp ~gzip:true xmlinnertypes (Some innertypespath); ensure_path_exists xmlpath; Xml.pp ~gzip:true xml (Some xmlpath) ; - (* now register to the getter *) - Http_getter.register' innertypesuri (path_scheme_of innertypespath); - Http_getter.register' uri (path_scheme_of xmlpath); (* we return a list of uri,path we registered/created *) (uri,xmlpath) :: (innertypesuri,innertypespath) :: (* now the optional body, both write and register *) @@ -136,15 +133,10 @@ let save_object_to_disk status uri obj = None,None -> [] | Some bodyxml,Some bodyuri-> ensure_path_exists xmlbodypath; - Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ; - Http_getter.register' bodyuri (path_scheme_of xmlbodypath); - [bodyuri,xmlbodypath] + Xml.pp ~gzip:true bodyxml (Some xmlbodypath); + [bodyuri, xmlbodypath] | _-> assert false) -let remove_object_from_disk uri path = - Sys.remove path; - Http_getter.unregister' uri - let add_obj uri obj status = let dbd = MatitaDb.instance () in let suri = UriManager.string_of_uri uri in @@ -186,13 +178,15 @@ let delta_status status1 status2 = let remove_coercion uri = CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri) +let safe_remove fname = if Sys.file_exists fname then Sys.remove fname + let time_travel ~present ~past = let list_of_objs_to_remove = List.rev (delta_status past present) in (* List.rev is just for the debugging code, which otherwise may list both * something.ind and something.ind#xpointer ... (ask Enrico :-) *) let debug_list = ref [] in List.iter (fun (uri,p) -> - remove_object_from_disk uri p; + safe_remove p; remove_coercion uri; (try CicEnvironment.remove_obj uri @@ -230,11 +224,9 @@ let time_travel ~present ~past = MatitaLog.debug "l2:"; List.iter MatitaLog.debug l2 - let remove uri = let derived_uris_of_uri uri = UriManager.innertypesuri_of_uri uri :: - UriManager.annuri_of_uri uri :: (match UriManager.bodyuri_of_uri uri with | None -> [] | Some u -> [u]) @@ -247,17 +239,10 @@ let remove uri = List.iter (fun uri -> (try - let path = - let path = Http_getter.resolve' (UriManager.strip_xpointer uri) in - assert (String.sub path 0 7 = "file://"); - String.sub path 7 (String.length path - 7) - in MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri); - remove_object_from_disk uri path; - with - Http_getter_types.Key_not_found _ -> Http_getter.unregister' uri); + safe_remove (Http_getter.resolve' uri) + with Http_getter_types.Key_not_found _ -> ()); remove_coercion uri; - ignore(MatitaDb.remove_uri uri)) + ignore (MatitaDb.remove_uri uri)) to_remove - - + diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index 06807a1e4..bb573fcb1 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -40,7 +40,6 @@ val alias_diff: from:MatitaTypes.status -> MatitaTypes.status -> val set_proof_aliases : MatitaTypes.status -> DisambiguateTypes.environment -> MatitaTypes.status - (* removes the object from DB, Disk, CoercionsDB, getter * asserts the uri is resolved to file:// so it is only for * user's objects *) diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index c16915e63..fbc393cfb 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -108,11 +108,6 @@ let main ~mode = MatitaDb.create_owner_environment (); *) status := Some (ref (Lazy.force MatitaEngine.initial_status)); - at_exit - (fun () -> - Http_getter_logger.log "Sync map tree to disk..."; - Http_getter.sync_dump_file (); - print_endline "\nThanks for using Matita!\n"); Sys.catch_break true; let fname = fname () in try @@ -173,8 +168,8 @@ let main ~mode = | CicTextualParser2.Parse_error (floc,err) -> let (x, y) = CicAst.loc_of_floc floc in MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); - Http_getter.sync_dump_file (); if mode = `COMPILER then exit 1 else pp_ocaml_mode () + diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 6a3ce06b3..f14c5e80e 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -1,11 +1,9 @@ -module HGT = Http_getter_types;; -module HG = Http_getter;; module UM = UriManager;; module TA = TacticAst;; let _ = Helm_registry.load_from "matita.conf.xml"; - HG.init (); + Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner") let main uri_to_remove = MatitacleanLib.clean_baseuris uri_to_remove @@ -19,11 +17,6 @@ let usage () = exit 1 let _ = - at_exit - (fun () -> - Http_getter_logger.log "Sync map tree to disk..."; - Http_getter.sync_dump_file (); - print_endline "\nThanks for using Matita!\n"); if Array.length Sys.argv < 2 then usage (); if Sys.argv.(1) = "all" then begin diff --git a/helm/matita/updater.ml b/helm/matita/updater.ml deleted file mode 100644 index 4a777e4d0..000000000 --- a/helm/matita/updater.ml +++ /dev/null @@ -1,10 +0,0 @@ -let main () = - Helm_registry.load_from "matita.conf.xml"; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - Http_getter.update (); - Http_getter.sync_dump_file () -;; - -main () - diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index 619e947f2..e4a840ccf 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -658,6 +658,13 @@ let end_element ctxt tag = (** {2 Parser internals} *) +let has_gz_suffix fname = + try + let idx = String.rindex fname '.' in + let suffix = String.sub fname idx (String.length fname - idx) in + suffix = ".gz" + with Not_found -> false + let parse uri filename = let ctxt = new_parser_context uri in ctxt.filename <- filename; @@ -671,7 +678,11 @@ let parse uri filename = ctxt.xml_parser <- Some xml_parser; try (try - P.parse xml_parser (`Gzip_file filename); + let xml_source = + if has_gz_suffix filename then `Gzip_file filename + else `File filename + in + P.parse xml_parser xml_source with exn -> ctxt.xml_parser <- None; (* ZACK: the above "<- None" is vital for garbage collection. Without it diff --git a/helm/ocaml/cic/test.ml b/helm/ocaml/cic/test.ml index d7b6c2575..134ff789d 100644 --- a/helm/ocaml/cic/test.ml +++ b/helm/ocaml/cic/test.ml @@ -67,9 +67,7 @@ let rec parse uri tmpfile1 tmpfile2 = when Str.string_match body_RE uri 0 -> parse uri tmpfile1 None | CicParser.Parser_failure msg -> - printf "%s FAILED (%s)\n" uri msg; flush stdout); - unlink tmpfile1; - (match tmpfile2 with None -> () | Some f -> unlink f) + printf "%s FAILED (%s)\n" uri msg; flush stdout) let _ = try diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 86b8dd921..1f2c6be0e 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -488,30 +488,11 @@ let get_object_to_add uri = match UriManager.bodyuri_of_uri uri with None -> None | Some bodyuri -> - try - ignore (Http_getter.resolve' bodyuri) ; - (* The body exists ==> it is not an axiom *) - Some (Http_getter.getxml' bodyuri) - with - Http_getter_types.Key_not_found _ -> - (* The body does not exist ==> we consider it an axiom *) + if Http_getter.exists' bodyuri then + Some (Http_getter.getxml' bodyuri) + else None in - let cleanup () = - Unix.unlink filename ; - (* - begin - match filename_univ with - Some f -> Unix.unlink f - | None -> () - end; - *) - begin - match bodyfilename with - Some f -> Unix.unlink f - | None -> () - end - in (* restarts the numbering of named universes (the ones inside the cic) *) let _ = CicUniv.restart_numbering () in let obj = @@ -522,13 +503,12 @@ let get_object_to_add uri = !total_parsing_time +. ((Unix.gettimeofday()) -. time ); rc with exn -> - cleanup (); (match exn with | CicParser.Getter_failure ("key_not_found", uri) -> raise (Object_not_found (UriManager.uri_of_string uri)) | _ -> raise exn) in - let ugraph,filename_univ = + let ugraph,filename_univ = (* FIXME: decomment this when the universes will be part of the library try let filename_univ = @@ -549,10 +529,8 @@ let get_object_to_add uri = ***********************************************) (Some CicUniv.empty_ugraph,None) in - cleanup(); - obj,ugraph - with - Http_getter_types.Key_not_found _ -> raise (Object_not_found uri) + obj,ugraph + with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri) ;; (* this is the function to fetch the object in the unchecked list and @@ -674,12 +652,7 @@ let in_cache uri = let add_type_checked_obj uri (obj,ugraph) = Cache.add_cooked ~key:uri (obj,ugraph) -let in_library uri = - in_cache uri || - (try - ignore (Http_getter.resolve' uri); - true - with Http_getter_types.Key_not_found _ -> false) +let in_library uri = in_cache uri || Http_getter.exists' uri let remove_obj = Cache.remove diff --git a/helm/ocaml/metadata/extractor/extractor_manager.ml b/helm/ocaml/metadata/extractor/extractor_manager.ml index ae541f458..05393b63e 100644 --- a/helm/ocaml/metadata/extractor/extractor_manager.ml +++ b/helm/ocaml/metadata/extractor/extractor_manager.ml @@ -172,7 +172,6 @@ let main () = Helm_registry.load_from "extractor.conf.xml"; Http_getter.init (); print_endline "Updating the getter...."; - Http_getter.update (); let base = (Helm_registry.get "tmp.dir") ^ "/maps" in let formats i = (Helm_registry.get "tmp.dir") ^ "/"^(string_of_int i)^"/maps" -- 2.39.2