beginning to see the light

[helm.git] / components / library / librarian.ml

diff --git a/components/library/librarian.ml b/components/library/librarian.ml
index f2268488f2afbc3ce975578c072a172af1ec72ac..db6b815746398f3c0305f5088f8c220316c12a03 100644 (file)
--- a/components/library/librarian.ml
+++ b/components/library/librarian.ml
@@ -1,3 +1,5 @@
+let debug = false;;
+
 exception NoRootFor of string
 
 let absolutize path =
@@ -52,7 +54,7 @@ let find_root_for ~include_paths file =
  try 
    let path = HExtlib.find_in include_paths file in
    let path = absolutize path in
-   (* HLog.debug ("file "^file^" resolved as "^path); *)
+(*     HLog.debug ("file "^file^" resolved as "^path);  *)
    let rootpath, root, buri = 
      try
        let mburi = Helm_registry.get "matita.baseuri" in
@@ -65,12 +67,13 @@ let find_root_for ~include_paths file =
        let buri = List.assoc "baseuri" (load_root_file rootpath) in
        rootpath, Filename.dirname rootpath, buri
    in
-   (* HLog.debug ("file "^file^" rooted by "^rootpath^""); *)
+(*     HLog.debug ("file "^file^" rooted by "^rootpath^"");  *)
    let uri = Http_getter_misc.strip_trailing_slash buri in
    if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
      HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
    ensure_trailing_slash root, remove_trailing_slash uri, path
  with Failure "find_in" -> 
+   HLog.error ("We are in: " ^ Sys.getcwd ());
    HLog.error ("Unable to find: "^file^"\nPaths explored:");
    List.iter (fun x -> HLog.error (" - "^x)) include_paths;
    raise (NoRootFor file)
@@ -90,7 +93,8 @@ let baseuri_of_script ~include_paths file =
   in
   let extra_buri = substract lpath lroot in
   let chop name = 
-    assert(Filename.check_suffix name ".ma");
+    assert(Filename.check_suffix name ".ma" ||
+      Filename.check_suffix name ".mma");
     try Filename.chop_extension name
     with Invalid_argument "Filename.chop_extension" -> name
   in
@@ -146,7 +150,7 @@ module type Format =
 
 module Make = functor (F:Format) -> struct
 
-  let prerr_endline _ = ();; 
+  let prerr_endline s = if debug then prerr_endline ("make: "^s);; 
 
   let younger_s_t a b = 
     match F.mtime_of_source_object a, F.mtime_of_target_object b with