X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=f248545fba8c6d5caae409eb43fee604273185b2;hb=7a3c40d0d56ba3c20126f1d2c9f651adc95eaef7;hp=b33590a0ae95127a7afb7ae0dff0576342626cb0;hpb=662f191b09d1b9e3d13e4f9ee5c174c1ac08fadb;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index b33590a0a..f248545fb 100644
--- 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 () 
@@ -259,11 +258,13 @@ let compile options fname =
      with MatitaEngine.EnrichedWithLexiconStatus 
             (GrafiteEngine.Macro (floc, f), lex_status) as exn ->
             match f (get_macro_context (Some grafite_status)) with 
-            | _, GrafiteAst.Inline (_, style, suri, prefix) ->
+            | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
               let str =
-               ApplyTransformation.txt_of_inline_macro style suri prefix
-                ~map_unicode_to_tex:(Helm_registry.get_bool
-                  "matita.paste_unicode_as_tex") in
+               ApplyTransformation.txt_of_inline_macro style prefix suri
+                ?flavour
+		~map_unicode_to_tex:(Helm_registry.get_bool
+                  "matita.paste_unicode_as_tex")
+	      in
               !out str;
               aux_for_dump x
             |_-> raise exn
@@ -279,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" && 
@@ -300,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
@@ -318,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 ->
@@ -341,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
@@ -348,34 +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
-	  atexit res
-       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