From a7f186ba154eae6a0e3fd61ecd6d1112daa994da Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 25 Jul 2005 17:16:17 +0000
Subject: [PATCH] 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.

---
 helm/matita/matita.txt       |  2 +-
 helm/matita/matitaGui.ml     | 25 ++++++++++++++++++++++++-
 helm/matita/matitaScript.ml  |  1 +
 helm/matita/matitaScript.mli |  1 +
 4 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 9026e63b3..253f10765 100644
--- 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 733d0aab9..6cc4731ad 100644
--- 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 811b1a858..af7b02a82 100644
--- 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 258a72e0c..2cc559a3b 100644
--- 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
-- 
2.39.2