More notation (up to where the open bugs allow me to put it without adding

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 216dc9d5b79d2cbef8536142a6332ffce2f20db8..6cc4731ad6e7503df7cfaa5521f8019d4729672f 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -355,9 +355,8 @@ class gui () =
         ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
       ignore(self#main#selectAllMenuItem#connect#activate
         ~callback:(fun () ->
-          source_buffer#move_mark `INSERT (source_buffer#get_iter `START);
-          source_buffer#move_mark `SEL_BOUND (source_buffer#get_iter `END)
-          ));
+          source_buffer#move_mark `INSERT source_buffer#start_iter;
+          source_buffer#move_mark `SEL_BOUND source_buffer#end_iter));
       ignore(self#main#findReplMenuItem#connect#activate
         ~callback:show_find_Repl);
       ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
@@ -375,8 +374,13 @@ class gui () =
       let locker f = 
         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
+      let keep_focus f =
+        fun () ->
+         try
+          f (); source_view#misc#grab_focus ()
+         with
+          exc -> source_view#misc#grab_focus (); raise exc in
         (* developments win *)
       let model = 
         new MatitaGtkMisc.multiStringListModel 
@@ -632,19 +636,17 @@ class gui () =
       in
       let cursor () =
         source_buffer#place_cursor
-          (source_buffer#get_iter_at_mark (`NAME "locked"));
-        source_view#misc#grab_focus ()
-      in
+          (source_buffer#get_iter_at_mark (`NAME "locked")) in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
-      let advance = locker advance in
-      let retract = locker retract in
-      let top = locker top in
-      let bottom = locker bottom in
-      let jump = locker jump in
+      let advance = locker (keep_focus advance) in
+      let retract = locker (keep_focus retract) in
+      let top = locker (keep_focus top) in
+      let bottom = locker (keep_focus bottom) in
+      let jump = locker (keep_focus jump) in
       let connect_key sym f =
         connect_key self#main#mainWinEventBox#event
           ~modifiers:[`CONTROL] ~stop:true sym f;
@@ -726,7 +728,30 @@ class gui () =
       self#main#hpaneScriptSequent#set_position script_w;
         (* source_view *)
       ignore(source_view#connect#after#paste_clipboard 
-        ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock))
+        ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock));
+      (* clean_locked is set to true only "during" a PRIMARY paste
+         operation (i.e. by clicking with the second mouse button) *)
+      let clean_locked = ref false in
+      ignore(source_view#event#connect#button_press
+        ~callback:
+          (fun button ->
+            if GdkEvent.Button.button button = 2 then
+             clean_locked := true;
+            false
+          ));
+      ignore(source_view#event#connect#button_release
+        ~callback:(fun button -> clean_locked := false; false));
+      ignore(source_view#buffer#connect#after#apply_tag
+       ~callback:(
+         fun tag ~start:_ ~stop:_ ->
+          if !clean_locked &&
+             tag#get_oid = (MatitaScript.instance ())#locked_tag#get_oid
+          then
+           begin
+            clean_locked := false;
+            (MatitaScript.instance ())#clean_dirty_lock;
+            clean_locked := true
+           end))
     
     method loadScript file =       
       let script = MatitaScript.instance () in