X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2Flibrarian.mli;h=4eed9051d459784866b28138523e29ff61bb8c25;hb=0ef9250d71eacd6b1022194128e6acfb74d52aac;hp=e7b6df521aaff07fe08b57d1fa2be9eabbdcf90d;hpb=7782637e13656ec7d1d0ccc84e0d8cf894431187;p=helm.git

diff --git a/helm/software/components/library/librarian.mli b/helm/software/components/library/librarian.mli
index e7b6df521..4eed9051d 100644
--- a/helm/software/components/library/librarian.mli
+++ b/helm/software/components/library/librarian.mli
@@ -70,11 +70,12 @@ 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, relative source, writeable target, read only target *)
+	   string option * source_object * 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
-    val dotdothack: source_object -> source_object 
   end
 
 module Make :
@@ -91,9 +92,14 @@ module Make :
  * state that plus.ma needs nat and equality
  *)
 val load_deps_file: string -> (string * string list) list
-val write_deps_file: string -> (string * string list) list -> unit
+val write_deps_file: string option -> (string * string list) list -> unit
 
 (* FG ***********************************************************************)
 
 (* true if the argunent starts with a uri scheme prefix *)
 val is_uri: string -> bool
+
+(* Valid values: 0: no debug; 1: normal debug; > 1: extra debug *)
+val debug: int ref
+
+val time_stamp: string -> unit