snopshot (working one!)

[helm.git] / components / library / librarySync.ml

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index c36d84c90dd88de02938fdef9507906a55659edb..630b51be8a59c4352cf4fe92bbf5d716f6891d1f 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -243,6 +243,29 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,_,_) -> true)
 
+let stack = ref [];;
+
+let h2l h =
+  UriManager.UriHashtbl.fold 
+  (fun k v acc -> (k,v) :: acc) h []
+;;
+
+let push () =
+  stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack;
+  remove_all_coercions ()
+;;
+
+let pop () =
+  match !stack with
+  | [] -> raise (Failure "Unable to POP from librarySync.ml")
+  | (db,h) :: tl -> 
+      stack := tl;
+      remove_all_coercions ();
+      CoercDb.restore db;
+      List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v)
+      h
+;;
+
 let add_coercion ~add_composites refinement_toolkit uri arity saturations
  baseuri
 =