X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=adb9bf753fc05fa9f05fa21be0451177383fc469;hb=e480ed0d9242f2e505cf28e175262c841bc470c2;hp=04b86d0b7caecce461ca1d179db63984fd67fd21;hpb=cbcd34fe15122eb9835a5226b98be1050b097d6a;p=helm.git

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 04b86d0b7..adb9bf753 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -70,47 +70,55 @@ let clean_current_baseuri grafite_status =
     with GrafiteTypes.Option_error _ -> ()
 
 let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = 
-  let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
-  let moo_fname = 
-    LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in
-  let save () =
-    let metadata_fname =
-     LibraryMisc.metadata_file_of_baseuri 
-       ~must_exist:false ~baseuri ~writable:true in
-    let lexicon_fname =
-     LibraryMisc.lexicon_file_of_baseuri 
-       ~must_exist:false ~baseuri ~writable:true
-    in
-     GrafiteMarshal.save_moo moo_fname
-      grafite_status.GrafiteTypes.moo_content_rev;
-     LibraryNoDb.save_metadata metadata_fname
-      lexicon_status.LexiconEngine.metadata;
-     LexiconMarshal.save_lexicon lexicon_fname
-      lexicon_status.LexiconEngine.lexicon_content_rev
+  let baseuri =
+   try Some (GrafiteTypes.get_string_option grafite_status "baseuri")
+   with GrafiteTypes.Option_error _ -> None
   in
   if (MatitaScript.current ())#eos &&
-     grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
+     grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof &&
+     baseuri <> None
   then
-    begin
-      let rc = 
-        MatitaGtkMisc.ask_confirmation
-        ~title:"A .moo can be generated"
-        ~message:(Printf.sprintf 
-          "%s can be generated for %s.\n<i>Should I generate it?</i>"
-          (Filename.basename moo_fname) (Filename.basename fname))
-        ~parent ()
-      in
-      let b = 
-        match rc with 
-        | `YES -> true 
-        | `NO -> false 
-        | `CANCEL -> raise MatitaTypes.Cancel 
+   begin
+    let baseuri = match baseuri with Some b -> b | None -> assert false in
+    let moo_fname = 
+     LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
+      ~writable:true in
+    let save () =
+      let metadata_fname =
+       LibraryMisc.metadata_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true in
+      let lexicon_fname =
+       LibraryMisc.lexicon_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true
       in
-      if b then
-          save ()
-      else
-        clean_current_baseuri grafite_status
-    end
+       GrafiteMarshal.save_moo moo_fname
+        grafite_status.GrafiteTypes.moo_content_rev;
+       LibraryNoDb.save_metadata metadata_fname
+        lexicon_status.LexiconEngine.metadata;
+       LexiconMarshal.save_lexicon lexicon_fname
+        lexicon_status.LexiconEngine.lexicon_content_rev
+    in
+     begin
+       let rc = 
+         MatitaGtkMisc.ask_confirmation
+         ~title:"A .moo can be generated"
+         ~message:(Printf.sprintf 
+           "%s can be generated for %s.\n<i>Should I generate it?</i>"
+           (Filename.basename moo_fname) (Filename.basename fname))
+         ~parent ()
+       in
+       let b = 
+         match rc with 
+         | `YES -> true 
+         | `NO -> false 
+         | `CANCEL -> raise MatitaTypes.Cancel 
+       in
+       if b then
+           save ()
+       else
+         clean_current_baseuri grafite_status
+     end
+   end
   else
     clean_current_baseuri grafite_status 
     
@@ -407,17 +415,42 @@ class gui () =
       let lock_world _ =
         main#buttonsToolbar#misc#set_sensitive false;
         develList#buttonsHbox#misc#set_sensitive false;
+        main#scriptMenu#misc#set_sensitive false;
         source_view#set_editable false
       in
       let unlock_world _ =
         main#buttonsToolbar#misc#set_sensitive true;
         develList#buttonsHbox#misc#set_sensitive true;
+        main#scriptMenu#misc#set_sensitive true;
         source_view#set_editable true
       in
-      let locker f = 
+      let worker_thread = ref None in
+      let locker f () =
+       let thread_main =
         fun () -> 
           lock_world ();
-          try f ();unlock_world () with exc -> unlock_world (); raise exc in
+          try f ();unlock_world () with exc -> unlock_world (); raise exc
+       in
+        worker_thread := Some (Thread.create thread_main ()) in
+      let kill_worker =
+       (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *)
+       let interrupt = ref None in
+       let old_callback = ref (function _ -> ()) in
+       let force_interrupt n =
+         (* This function is called just before the thread's timeslice ends *)
+         !old_callback n;
+         if Some(Thread.id(Thread.self())) = !interrupt then
+          (interrupt := None; raise Sys.Break) in
+       let _ =
+        match Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) with
+           Sys.Signal_handle f -> old_callback := f
+         | Sys.Signal_ignore
+         | Sys.Signal_default -> assert false
+       in
+        fun () ->
+         match !worker_thread with
+            None -> assert false
+          | Some t -> interrupt := Some (Thread.id t) in
       let keep_focus f =
         fun () ->
          try
@@ -478,10 +511,19 @@ class gui () =
           match get_devel_selected () with
           | None -> ()
           | Some d -> 
-              let clean = locker 
-                (fun () -> MatitamakeLib.publish_development_in_bg refresh d)
-              in
-              ignore(clean ())));
+              let publish = locker (fun () ->
+                MatitamakeLib.publish_development_in_bg refresh d) in
+              ignore(publish ())));
+      connect_button develList#graphButton (fun () -> 
+        match get_devel_selected () with
+        | None -> ()
+        | Some d ->
+            (match MatitamakeLib.dot_for_development d with
+            | None -> ()
+            | Some _ ->
+                let browser = MatitaMathView.cicBrowser () in
+                browser#load (`Development
+                  (MatitamakeLib.name_for_development d))));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
@@ -604,7 +646,7 @@ class gui () =
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
+      connect_button tbar#autoButton (tac (A.Auto (loc,[])));
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:main#tacticsBarMenuItem;
@@ -781,6 +823,7 @@ class gui () =
       connect_button main#scriptTopButton top;
       connect_button main#scriptBottomButton bottom;
       connect_button main#scriptJumpButton jump;
+      connect_button main#scriptAbortButton kill_worker;
       connect_menu_item main#scriptAdvanceMenuItem advance;
       connect_menu_item main#scriptRetractMenuItem retract;
       connect_menu_item main#scriptTopMenuItem top;
@@ -895,7 +938,7 @@ class gui () =
         source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
       in
       let get_ligature word =
-        let len = MatitaGtkMisc.utf8_string_length word in
+        let len = String.length word in
         let aux_tex () =
           try
             for i = len - 1 downto 0 do
@@ -999,16 +1042,34 @@ class gui () =
     method loadScript file =       
       let script = MatitaScript.current () in
       script#reset (); 
-      script#assignFileName file;
-      let content =
-       if Sys.file_exists file then file
-       else BuildTimeConf.script_template
-      in
-       source_view#source_buffer#begin_not_undoable_action ();
-       script#loadFromFile content;
-       source_view#source_buffer#end_not_undoable_action ();
-       console#message ("'"^file^"' loaded.");
-       self#_enableSaveTo file
+      if Pcre.pmatch ~pat:"\\.p$" file then
+        begin
+          let tptppath = 
+            Helm_registry.get_opt_default Helm_registry.string ~default:"./"
+              "matita.tptppath"
+          in
+          let data = Matitaprover.p_to_ma ~filename:file ~tptppath () in
+          let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in
+          script#assignFileName filename;
+          source_view#source_buffer#begin_not_undoable_action ();
+          script#loadFromString data;
+          source_view#source_buffer#end_not_undoable_action ();
+          console#message ("'"^filename^"' loaded.");
+          self#_enableSaveTo filename
+        end
+      else
+        begin
+          script#assignFileName file;
+          let content =
+           if Sys.file_exists file then file
+           else BuildTimeConf.script_template
+          in
+           source_view#source_buffer#begin_not_undoable_action ();
+           script#loadFromFile content;
+           source_view#source_buffer#end_not_undoable_action ();
+           console#message ("'"^file^"' loaded.");
+           self#_enableSaveTo file
+        end
       
     method setStar name b =
       let l = main#scriptLabel in