1) NCicTypechecker.typecheck_obj removed, since it did not add to the

[helm.git] / helm / software / components / ng_kernel / nCicLibrary.ml

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 98f8903d8a5d3783852e92705fc7ff667ae46d7d..1efe173e73620db5c17b3bdd23f781355e2bab4c 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -77,6 +77,7 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
   Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) [];
   close_out ch in
  let load_db () =
+  HExtlib.mkdir (Helm_registry.get "matita.basedir");
   try
    let ga,im = require_path (db_path ()) in
    let ga =
@@ -137,7 +138,12 @@ class status =
 
 let time_travel status =
  let sto,ali,cac,inc = status#timestamp in
-  storage := sto; local_aliases := ali; cache := cac; includes := inc
+  let diff_len = List.length !storage - List.length sto in
+  let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in
+   if List.length to_be_deleted > 0 then
+    let u,_ = HExtlib.list_last to_be_deleted in
+     NCicEnvironment.invalidate_obj u;
+   storage := sto; local_aliases := ali; cache := cac; includes := inc
 ;;
 
 let serialize ~baseuri dump =
@@ -248,7 +254,8 @@ let aliases_of uri =
   Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri)))
 ;;
 
-let add_obj status u obj =
+let add_obj status ((u,_,_,_,_) as obj) =
+ NCicEnvironment.check_and_add_obj obj;
  storage := (u,obj)::!storage;
   let _,height,_,_,obj = obj in
   let references =