X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaGui.ml;h=38f8cb7849da4d1af0d5cbf2c5328454c6e8f4da;hb=5022202a659044d981833ba8665424a52684b07f;hp=51b17451e9caa1c1bbd9d964930dcd46368dd61b;hpb=619a3a478a4f6b0a50782b620009f6a141c30a53;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 51b17451e..38f8cb784 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -170,7 +170,8 @@ class gui () =
       let find_forward _ = 
           let highlight start end_ =
             source_buffer#move_mark `INSERT ~where:start;
-            source_buffer#move_mark `SEL_BOUND ~where:end_
+            source_buffer#move_mark `SEL_BOUND ~where:end_;
+            source_view#scroll_mark_onscreen `INSERT
           in
           let text = findRepl#findEntry#text in
           let iter = source_buffer#get_iter `SEL_BOUND in
@@ -196,6 +197,64 @@ class gui () =
       connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
       ignore(findRepl#toplevel#event#connect#delete 
         ~callback:(fun _ -> hide_find_Repl ();true));
+      ignore(self#main#undoMenuItem#connect#activate
+        ~callback:(fun () ->
+          (* phase 1: we save the actual status of the marks and we undo *)
+          let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+          let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+          let locked_iter_offset = locked_iter#offset in
+          let mark2 =
+           `MARK
+             (source_view#buffer#create_mark ~name:"lock_point"
+               ~left_gravity:true locked_iter) in
+          source_view#source_buffer#undo ();
+          (* phase 2: we save the cursor position and we redo, restoring
+             the previous status of all the marks *)
+          let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+          let mark =
+           `MARK
+             (source_view#buffer#create_mark ~name:"undo_point"
+               ~left_gravity:true cursor_iter)
+          in
+           source_view#source_buffer#redo ();
+           let mark_iter = source_view#buffer#get_iter_at_mark mark in
+           let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+           let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+            source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+            source_view#buffer#delete_mark mark;
+            source_view#buffer#delete_mark mark2;
+            (* phase 3: if after the undo the cursor was in the locked area,
+               then we move it there again and we perform a goto *)
+            if mark_iter#offset < locked_iter_offset then
+             begin
+              source_view#buffer#move_mark `INSERT ~where:mark_iter;
+              source_view#buffer#move_mark `SEL_BOUND ~where:mark_iter;
+              (MatitaScript.instance ())#goto `Cursor ();
+             end;
+            (* phase 4: we perform again the undo. This time we are sure that
+               the text to undo is not locked *)
+            source_view#source_buffer#undo ();
+            source_view#misc#grab_focus ()
+         ));
+      ignore(source_view#source_buffer#connect#can_undo
+        ~callback:self#main#undoMenuItem#misc#set_sensitive);
+      ignore(self#main#redoMenuItem#connect#activate
+        ~callback:source_view#source_buffer#redo);
+      ignore(source_view#source_buffer#connect#can_redo
+        ~callback:self#main#redoMenuItem#misc#set_sensitive);
+      let clipboard =
+       let atom = Gdk.Atom.clipboard in
+        GData.clipboard atom in
+      ignore(self#main#cutMenuItem#connect#activate
+        ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard));
+      ignore(self#main#copyMenuItem#connect#activate
+        ~callback:(fun () -> source_view#buffer#copy_clipboard clipboard));
+      ignore(self#main#pasteMenuItem#connect#activate
+        ~callback:(fun () ->
+          source_view#buffer#paste_clipboard clipboard;
+          (MatitaScript.instance ())#clean_dirty_lock));
+      ignore(self#main#deleteMenuItem#connect#activate
+        ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
       ignore(self#main#findReplMenuItem#connect#activate
         ~callback:show_find_Repl);
       ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
@@ -225,16 +284,21 @@ class gui () =
           | None -> ()
           | Some d -> MatitamakeLib.destroy_development d);
           refresh_devels_win ());
+      let refresh () = 
+        while Glib.Main.pending () do 
+          ignore(Glib.Main.iteration false); 
+        done
+      in
       connect_button develList#buildButton 
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.build_development d));
+          | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
       connect_button develList#cleanButton 
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.clean_development d));
+          | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
@@ -322,19 +386,20 @@ class gui () =
                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
         (* toolbar *)
-      let module A = TacticAst in
-      let hole = CicAst.UserInput in
-      let loc = CicAst.dummy_floc in
+      let module A = GrafiteAst in
+      let hole = CicNotationPt.UserInput in
+      let loc = Disambiguate.dummy_floc in
       let tac ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
           (MatitaScript.instance ())#advance
-            ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
+            ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+            ()
       in
       let tac_w_term ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
           let buf = source_buffer in
           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
-            ("\n" ^ TacticAstPp.pp_tactic ast)
+            ("\n" ^ GrafiteAstPp.pp_tactic ast)
       in
       let tbar = self#main in
       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
@@ -423,15 +488,19 @@ class gui () =
           | Some f -> 
                 script#reset (); 
                 script#assignFileName f;
+                source_view#source_buffer#begin_not_undoable_action ();
                 script#loadFromFile (); 
+                source_view#source_buffer#end_not_undoable_action ();
                 console#message ("'"^f^"' loaded.\n");
                 self#_enableSaveTo f
           | None -> ()
         with MatitaTypes.Cancel -> ()
       in
       let newScript () = 
+        source_view#source_buffer#begin_not_undoable_action ();
         (s ())#reset (); 
         (s ())#template (); 
+        source_view#source_buffer#end_not_undoable_action ();
         disableSave ();
         script_fname <- None
       in
@@ -556,7 +625,9 @@ class gui () =
           output_string oc template;
           close_out oc
         end;
+      source_view#source_buffer#begin_not_undoable_action ();
       script#loadFromFile ();
+      source_view#source_buffer#end_not_undoable_action ();
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file