]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/librarian.mli
librarian.ml: now the read_only .moo's are managed "correctly" (i.e. better than...
[helm.git] / helm / software / components / library / librarian.mli
index c682579c2352845cb4886cf87d462a6d291a94e7..0e15e28bcc78dc5b88bdff6bc208e22d4939d23e 100644 (file)
@@ -70,7 +70,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
@@ -90,5 +92,13 @@ 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
+
+val debug: bool ref
+
+val time_stamp: string -> unit