From: Enrico Tassi Date: Wed, 13 Jul 2005 09:26:52 +0000 (+0000) Subject: copied text is unlocked :) X-Git-Tag: pre_notation~25 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7aa0e7901b71a660c6d6f55d96a38a3a9d1d3c7d;p=helm.git copied text is unlocked :) --- 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