X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2Flibrarian.ml;h=62a8a892c3887f5b965266e49077846456ffa227;hb=b91dfc5e2b00e6b0b4cb81109192bb2b825055a1;hp=4c222b0b936692fa0d22a76f0d0739c861f195dd;hpb=2ce98fa7862b4cb93f7e62d1474092bece17c1d0;p=helm.git

diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index 4c222b0b9..62a8a892c 100644
--- a/helm/software/components/library/librarian.ml
+++ b/helm/software/components/library/librarian.ml
@@ -191,7 +191,9 @@ module type Format =
     val string_of_target_object: target_object -> string
     val build: options -> source_object -> bool
     val root_and_target_of: 
-          options -> source_object -> string option * target_object
+          options -> source_object -> 
+	   (* root, writeable target, read only target *)
+	   string option * target_object * target_object
     val mtime_of_source_object: source_object -> float option
     val mtime_of_target_object: target_object -> float option
     val is_readonly_buri_of: options -> source_object -> bool
@@ -209,10 +211,10 @@ module Make = functor (F:Format) -> struct
   let fst4 = function (x,_,_,_) -> x;;
 
   let modified_before_s_t (_,cs, ct, _, _) a b = 
-(*    
+(*   
     time_stamp ("L s_t: a " ^ F.string_of_source_object a);
     time_stamp ("L s_t: b " ^ F.string_of_target_object b);
-*)
+*)    
     let a = try Hashtbl.find cs a with Not_found -> assert false in
     let b = 
       try
@@ -230,16 +232,16 @@ module Make = functor (F:Format) -> struct
        | Some a, Some b -> a <= b
        | _ -> false
     in
-(*    
+(*
     time_stamp ("L s_t: " ^ string_of_bool r);
-*)    
+*)
     r
 
   let modified_before_t_t (_,_,ct, _, _) a b =
-(*    
+(*
     time_stamp ("L t_t: a " ^ F.string_of_target_object a);
     time_stamp ("L t_t: b " ^ F.string_of_target_object b);
-*) 
+*)    
     let a = 
       try
         match Hashtbl.find ct a with
@@ -266,16 +268,16 @@ module Make = functor (F:Format) -> struct
     in
     let r = match a, b with
        | Some a, Some b ->
-(*       
+(*
        time_stamp ("tt: a " ^ string_of_float a);
        time_stamp ("tt: b " ^ string_of_float b);
-*)       
+*)
           a <= b
        | _ -> false
     in
-(*    
+(*
     time_stamp ("L t_t: " ^ string_of_bool r);
-*)    
+*)
     r
 
   let rec purge_unwanted_roots wanted deps =
@@ -420,10 +422,9 @@ module Make = functor (F:Format) -> struct
 		   let res = F.build lo t in
 		   time_stamp ("L : DONE     " ^ str); res
 		end else begin
-                   Hashtbl.remove ct tgt;
-                   Hashtbl.add ct tgt None;
-		   HLog.warn("Read only baseuri for: "^ str^
-                     ", assuming it is aleary built."); true
+		   HLog.error ("Read only baseuri for: "^ str^
+                     ", I won't compile it even if it is out of date"); 
+		   false
 		end
              | Some froot -> make froot [t]
              | None -> 
@@ -449,11 +450,21 @@ module Make = functor (F:Format) -> struct
     let deps = 
       List.map 
         (fun (file,d) -> 
-          let r,tgt = F.root_and_target_of local_options file in
+          let r,wtgt,rotgt = F.root_and_target_of local_options file in
           Hashtbl.add caches file (F.mtime_of_source_object file);
-          Hashtbl.add cachet tgt (F.mtime_of_target_object tgt); 
-          Hashtbl.add cached file (file, d, r, tgt);
-          (file, d, r, tgt)
+	  (* if a read only target exists, we use that one, otherwise
+	     we use the writeable one that may be compiled *)
+	  let _,_,_, tgt as tuple = 
+	    match F.mtime_of_target_object rotgt with
+	    | Some _ as mtime ->
+               Hashtbl.add cachet rotgt mtime; 
+	       (file, d, r, rotgt)
+	    | None -> 
+               Hashtbl.add cachet wtgt (F.mtime_of_target_object wtgt); 
+	       (file, d, r, wtgt)
+	  in
+          Hashtbl.add cached file tuple;
+          tuple
 	)
         deps
     in