librarian.ml: now the read_only .moo's are managed "correctly" (i.e. better than...

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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 9c331d2ee2da2bf2a0bc9d692aa9c58543c4f451..f248545fba8c6d5caae409eb43fee604273185b2 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -198,7 +198,6 @@ let compile options fname =
     CicNotation2.load_notation ~include_paths:[]
       BuildTimeConf.core_notation_script 
   in
-  let initial_lexicon_status = lexicon_status in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -281,8 +280,10 @@ let compile options fname =
      (HLog.error
       "there are still incomplete proofs at the end of the script"; 
      pp_times fname false big_bang big_bang_u big_bang_s;
+(*
      LexiconSync.time_travel 
        ~present:lexicon_status ~past:initial_lexicon_status;
+*)
      clean_exit baseuri false)
     else
      (if not (Helm_registry.get_bool "matita.moo" && 
@@ -302,15 +303,19 @@ let compile options fname =
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
      pp_times fname true big_bang big_bang_u big_bang_s;
+(*
      LexiconSync.time_travel 
        ~present:lexicon_status ~past:initial_lexicon_status;
+*)
      true)
   with 
   (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
   | AttemptToInsertAnAlias lexicon_status -> 
      pp_times fname false big_bang big_bang_u big_bang_s;
+(*
      LexiconSync.time_travel 
        ~present:lexicon_status ~past:initial_lexicon_status;
+*)
      clean_exit baseuri false
   | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) as exn' ->
       (match exn with
@@ -320,7 +325,8 @@ let compile options fname =
           HLog.error (sprintf "Parse error at %d-%d: %s" x y err)
       | exn when matita_debug -> raise exn'
       | exn -> HLog.error (snd (MatitaExcPp.to_string exn)));
-      LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
+(*       LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
+ *       *)
       pp_times fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri false
   | Sys.Break when not matita_debug ->
@@ -343,6 +349,7 @@ module F =
     let is_readonly_buri_of opts file = 
      let buri = List.assoc "baseuri" opts in
      Http_getter_storage.is_read_only (Librarian.mk_baseuri buri file)
+    ;;
 
     let root_and_target_of opts mafile = 
       try
@@ -350,38 +357,62 @@ module F =
         let root,baseuri,_,_ =
           Librarian.baseuri_of_script ~include_paths mafile 
         in
-       let obj =
-          if Filename.check_suffix mafile ".mma" then 
-             Filename.chop_suffix mafile ".mma" ^ ".ma"
-          else
-             LibraryMisc.obj_file_of_baseuri 
-                 ~must_exist:false ~baseuri ~writable:true
-       in
-        Some root, obj 
-      with Librarian.NoRootFor x -> None, ""
+        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,
+              LibraryMisc.obj_file_of_baseuri 
+                        ~must_exist:false ~baseuri ~writable:false
+        in
+        Some root, obj_writeable, obj_read_only
+      with Librarian.NoRootFor x -> None, "", ""
+    ;;
 
     let mtime_of_source_object s =
       try Some (Unix.stat s).Unix.st_mtime
       with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+    ;;
 
     let mtime_of_target_object s =
       try Some (Unix.stat s).Unix.st_mtime
       with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+    ;;
 
     let build options fname =
-       if Filename.check_suffix fname ".mma" then 
-          let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
-         let atexit = dump generated in
-         let res = compile options fname in
-         let r = atexit res in
-         if r then r else begin
-            Sys.remove generated;
-            Printf.printf "rm %s\n" generated; flush stdout; r
-         end
-       else
-          compile options fname
+      let compile opts fname =
+        try
+          GrafiteSync.push ();
+          GrafiteParser.push ();
+          let rc = compile opts fname in
+          GrafiteParser.pop ();
+          GrafiteSync.pop ();
+          rc
+        with 
+        | Sys.Break ->
+            GrafiteParser.pop ();
+            GrafiteSync.pop ();
+            false
+        | exn ->
+            HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
+            assert false
+      in
+      if Filename.check_suffix fname ".mma" then 
+         let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
+         let atexit = dump generated in
+         let res = compile options fname in
+         let r = atexit res in
+         if r then r else begin
+           Sys.remove generated;
+           Printf.printf "rm %s\n" generated; flush stdout; r
+         end
+      else
+         compile options fname
+    ;;
 
-    let load_deps_file = Librarian.load_deps_file
+    let load_deps_file = Librarian.load_deps_file;;
 
   end