From 1e2ad3511cad89d422ccd0bc46939522c846e56d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 25 Jul 2005 13:35:24 +0000 Subject: [PATCH] The edit menu items (copy/cut/delete/paste) are now sensitive to the selection/existence of textual data in the clipboard. --- helm/matita/matita.txt | 4 ++-- helm/matita/matitaGui.ml | 12 ++++++++++++ 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 9372b0a12..c08253e82 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -59,8 +59,7 @@ TODO - 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 - - sensitiveness per copy/paste/cut/delete nel menu Edit - - sensitiveness per goto begin/end/etc. + - sensitiveness per goto begin/end/etc. (???) - menu contestuale (tasto dx) nel sequent viewer - feedback su hyperlink nei sequenti e nel browser: rendere visibili gli @@ -81,6 +80,7 @@ TODO - non chiudere transitivamente i moo ?? DONE +- sensitiveness per copy/paste/cut/delete nel menu Edit -> CSC - fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza salvare. In verita' foo e' stato scritto lo stesso! -> CSC - matitaclean deve rimuovere anche i .moo; in alternativa il makefile diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index f83e01913..7eaf239e1 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -331,6 +331,18 @@ class gui () = let clipboard = let atom = Gdk.Atom.clipboard in GData.clipboard atom in + ignore(self#main#editMenu#connect#activate + ~callback: + (fun () -> + let something_selected = + (source_buffer#get_iter_at_mark `INSERT)#compare + (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0 + in + self#main#cutMenuItem#misc#set_sensitive something_selected; + self#main#copyMenuItem#misc#set_sensitive something_selected; + self#main#deleteMenuItem#misc#set_sensitive something_selected; + self#main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None) + )); ignore(self#main#cutMenuItem#connect#activate ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard)); ignore(self#main#copyMenuItem#connect#activate -- 2.39.2