...

[helm.git] / helm / software / matita / matitacLib.ml

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 70ed5766d273f35db6dbf293aa5313519993faac..a9172cee5a563b43406d37873a7eea76a72ee354 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -357,15 +357,18 @@ module F =
         let root,baseuri,_,_ =
           Librarian.baseuri_of_script ~include_paths mafile 
         in
-        let obj =
+        let obj_writeable, obj_read_only =
            if Filename.check_suffix mafile ".mma" then 
+              Filename.chop_suffix mafile ".mma" ^ ".ma",
               Filename.chop_suffix mafile ".mma" ^ ".ma"
            else
               LibraryMisc.obj_file_of_baseuri 
-                        ~must_exist:false ~baseuri ~writable:true
+                        ~must_exist:false ~baseuri ~writable:true,
+              LibraryMisc.obj_file_of_baseuri 
+                        ~must_exist:false ~baseuri ~writable:false
         in
-        Some root, obj 
-      with Librarian.NoRootFor x -> None, ""
+        Some root, obj_writeable, obj_read_only
+      with Librarian.NoRootFor x -> None, "", ""
     ;;
 
     let mtime_of_source_object s =
@@ -379,6 +382,7 @@ module F =
     ;;
 
     let build options fname =
+      let matita_debug = Helm_registry.get_bool "matita.debug" in
       let compile opts fname =
         try
           GrafiteSync.push ();
@@ -392,7 +396,7 @@ module F =
             GrafiteParser.pop ();
             GrafiteSync.pop ();
             false
-        | exn ->
+        | exn when not matita_debug ->
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
             assert false
       in