synchronisation Require

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@941 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 5 deletions

diff --git a/library/library.ml b/library/library.ml
index 558052a11..da7d01895 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -172,16 +172,28 @@ let load_module s = function
   | Some f -> let _ = load_module_from s f in ()
 
 
-(*s [require_module] loads and opens a module. *)
+(*s [require_module] loads and opens a module. This is a synchronized
+    operation. *)
 
-let require_module spec name fileopt export =
-  let file = match fileopt with
-    | None -> name
-    | Some f -> f in
+let cache_require (_,(name,file,export)) =
   let m = load_module_from name file in
   open_module name;
   if export then m.module_exported <- true
 
+let (in_require, _) =
+  declare_object
+    ("REQUIRE",
+     { cache_function = cache_require;
+       load_function = (fun _ -> ());
+       open_function = (fun _ -> ());
+       export_function = (fun _ -> None) })
+  
+let require_module spec name fileopt export =
+  let file = match fileopt with
+    | None -> name
+    | Some f -> f 
+  in
+  add_anonymous_leaf (in_require (name,file,export))
 
 (*s [save_module s] saves the module [m] to the disk. *)