From 7aa0e7901b71a660c6d6f55d96a38a3a9d1d3c7d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 13 Jul 2005 09:26:52 +0000
Subject: [PATCH] copied text is unlocked :)

---
 helm/matita/matita.txt       | 4 ++--
 helm/matita/matitaGui.ml     | 5 ++++-
 helm/matita/matitaScript.ml  | 9 ++++++++-
 helm/matita/matitaScript.mli | 3 +++
 4 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 5f213100a..9b49a1799 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -57,8 +57,6 @@ TODO
     su bisognerebbe tornare su di un passo e non fare undo degli alias
     (Zack: nella history ci sono anche gli offset per sapere a che pezzo di
     script uno stato appartiene)
-  - Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo
-    lockato!
   - keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre
     finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il
     codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare
@@ -88,6 +86,8 @@ TODO
     ( -I ?? o chiedere a matitamake la root e farci una find? )
 
 DONE
+- Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo
+  lockato! -> Gares
 - Bug: non disambigua
   inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
   perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 5ea390383..0d0fa1ba8 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -383,7 +383,10 @@ class gui () =
       let main_h = height * 80 / 100 in
       let script_w = main_w * 6 / 10 in
       self#main#toplevel#resize ~width:main_w ~height:main_h;
-      self#main#hpaneScriptSequent#set_position script_w  
+      self#main#hpaneScriptSequent#set_position script_w;
+        (* source_view *)
+      ignore(source_view#connect#after#paste_clipboard 
+        ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock))
     
     method loadScript file =       
       let script = MatitaScript.instance () in
diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 7aa31d33b..af38ff8c2 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -346,7 +346,7 @@ object (self)
 
   (** goal as seen by the user (i.e. metano corresponding to current tab) *)
   val mutable userGoal = ~-1
-
+  val mutable lock_mark_pos = 0
 
   (** text mark and tag representing locked part of a script *)
   val locked_mark =
@@ -413,6 +413,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
       ~stop:buffer#end_iter ()
 
+      
   (** @param rel_offset relative offset from current position of locked_mark *)
   method private moveMark rel_offset =
     let mark = `MARK locked_mark in
@@ -427,6 +428,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     in
     buffer#move_mark mark ~where:new_mark_pos;
     buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
+    lock_mark_pos <- new_mark_pos#offset;
     buffer#move_mark `INSERT old_insert;
     begin
      match self#status.proof_status with
@@ -435,6 +437,11 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     end ;
     while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
 
+  method clean_dirty_lock =
+    let lock_mark_iter = buffer#get_iter (`OFFSET lock_mark_pos) in
+    buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
+    buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:lock_mark_iter
+
   val mutable observers = []
 
   method addObserver (o: MatitaTypes.status -> unit) =
diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index cbdfb286b..ab39b9cfd 100644
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -60,6 +60,9 @@ object
 
   (** end of script, true if the whole script has been executed *)
   method eos: bool
+
+  (** misc *)
+  method clean_dirty_lock: unit
   
   (* debug *)
   method dump : unit -> unit
-- 
2.39.2