]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/librarian.mli
huge amount of work to make out Make crawl roots and
[helm.git] / components / library / librarian.mli
index 90b7ef168e64a265a1f24400a4846fa5ea2c0568..839d8daa1e80381b3aba4faed09bee8a520cf471 100644 (file)
@@ -2,7 +2,7 @@ exception NoRootFor of string
 
 val find_root: string -> string
 
-val parse_root: string -> (string*string) list
+(* val parse_root: string -> (string*string) list *)
 
 (* baseuri_of_script ?(inc:REG[matita.includes]) fname 
  *   -> 
@@ -10,7 +10,34 @@ val parse_root: string -> (string*string) list
  * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a,
  * /home/pippo/devel/a.ma *)
 val baseuri_of_script: 
-  ?include_paths:string list -> string -> string * string * string * string
+  include_paths:string list -> string -> string * string * string * string
 
 (* finds all the roots files in the specified dir *)
 val find_roots_in_dir: string -> string list
+
+(* make *)
+type options = (string * string) list
+
+module type Format =
+  sig
+    type source_object
+    type target_object
+    val load_deps_file: string -> (source_object * source_object list) list
+    val target_of: options -> source_object -> target_object
+    val string_of_source_object: source_object -> string
+    val string_of_target_object: target_object -> string
+    val build: options -> source_object -> bool
+    val root_of: options -> source_object -> string option
+    val mtime_of_source_object: source_object -> float option
+    val mtime_of_target_object: target_object -> float option
+  end
+
+module Make :
+  functor (F : Format) ->
+    sig
+      (* make [root dir] [targets], targets = [] means make all *)
+      val make : string -> F.source_object list ->  bool
+    end
+
+val load_deps_file: string -> (string * string list) list
+val write_deps_file: string -> (string * string list) list -> unit