class virtual status =
object
- inherit NCicExtraction.status
+ inherit NCic.status
val timestamp = (time0 : timestamp)
method timestamp = timestamp
method set_timestamp v = {< timestamp = v >}
- (*CSC: bug here, we are not copying the NCicExtraction part of the status *)
end
let time_travel0 (sto,ali) =
status#set_dump {status#dump with objs = obj::status#dump.objs }
;;
+let remove_objects ~baseuri =
+ let uri = NUri.string_of_uri baseuri in
+ let path = String.sub uri 4 (String.length uri - 4) in
+ let path = Helm_registry.get "matita.basedir" ^ path in
+ let map name = Sys.remove (Filename.concat path name) in
+ if HExtlib.is_dir path && HExtlib.is_regular (path ^ ".ng") then begin
+ HLog.warn ("removing contents of baseuri: " ^ uri);
+ Array.iter map (Sys.readdir path)
+ end
+
module type SerializerType =
sig
type dumpable_status
let ch = open_out (ng_path_of_baseuri baseuri) in
Marshal.to_channel ch (magic,(status#dump.dependencies,status#dump.objs)) [];
close_out ch;
+(*
+ remove_objects ~baseuri; (* FG: we remove the old objects before putting the new ones*)
+*)
List.iter
(function
| `Obj (uri,obj) ->
) il)
in
local_aliases := references @ !local_aliases;
- let status = status#set_timestamp (!storage,!local_aliases) in
- (* To test extraction *)
- try
- ignore (Helm_registry.get "extract_haskell");
- let status,msg = NCicExtraction.haskell_of_obj status orig_obj in
- prerr_endline msg; status
- with
- Helm_registry.Key_not_found _ -> status
+ status#set_timestamp (!storage,!local_aliases)
;;
let add_constraint status u1 u2 =
raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u)))
;;
-NCicEnvironment.set_get_obj get_obj;;
+NCicEnvironment.set_get_obj get_obj