Bug solved: X-style paste (i.e. paste of the PRIMARY selection using the

second mouse button) used to paste locked text as locked text.

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 9026e63b34acc4353543d350f63317c808ea4092..253f107650f89d119653a62d770e69fc68362efd 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -46,7 +46,6 @@ TODO
 
 
   GUI GRAFICA
-  - cut&paste stile "X": rimane la parte blu e lockata!
   - integrare il famoso logo mancante (anche nell'About dialog)
   - invertibilita' dell'inserimento automatico di alias: quando si torna
     su bisognerebbe tornare su di un passo e non fare undo degli alias
@@ -76,6 +75,7 @@ TODO
   - non chiudere transitivamente i moo ?? 
 
 DONE
+- cut&paste stile "X": rimane la parte blu e lockata! -> CSC
 - highlight degli errori di parsing nello script -> CSC
 - quando si fa una locate nel cicbrowser viene mangiato un pezzo di testo
   dalla finestra principale!!! -> CSC

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 733d0aab9699e37a5fd59fb9168a96dc674a10af..6cc4731ad6e7503df7cfaa5521f8019d4729672f 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -728,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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 811b1a858a4b98f873445d76ee4d247d08f8f834..af7b02a82f70a9e6765562b44413ca125418a13d 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -467,6 +467,7 @@ object (self)
   val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]
 
   method locked_mark = locked_mark
+  method locked_tag = locked_tag
 
     (* history can't be empty, the invariant above grant that it contains at
      * least the init status *)

diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index 258a72e0c13fc3cc748e578073a0ef12dcfcb92e..2cc559a3b0a790e751c8f9e466b90129eb3a329f 100644 (file)
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -27,6 +27,7 @@ class type script =
 object
 
   method locked_mark : Gtk.text_mark
+  method locked_tag : GText.tag
 
   (** @return current status *)
   method status: MatitaTypes.status