copied text is unlocked :)

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 5ea3903835f05dafa4a83dc4c6b2711b84aa3a5d..0d0fa1ba8c863df9bcd689054eb16a88e8f1f8fa 100644 (file)
--- 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