all pullbacks are attempted in sequence, removed many unfold

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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 70ed5766d273f35db6dbf293aa5313519993faac..ff9fb1d73629a468b1cde028505c56eb7385a6e3 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -180,10 +180,10 @@ let activate_extraction baseuri fname =
   let f =
     open_out
      (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
-   LibrarySync.set_object_declaration_hook
-    (fun _ obj ->
+   LibrarySync.add_object_declaration_hook
+    (fun ~add_obj ~add_coercion _ obj ->
       output_string f (CicExportation.ppobj baseuri obj);
-      flush f);
+      flush f; []);
 ;;
 
 let compile options fname =
@@ -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