+
+ (** selections / clipboards handling *)
+
+ method private markup_selected = MatitaMathView.has_selection ()
+ method private text_selected =
+ (source_buffer#get_iter_at_mark `INSERT)#compare
+ (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+ method private something_selected =
+ self#markup_selected || self#text_selected
+ method private markup_stored = MatitaMathView.has_clipboard ()
+ method private text_stored = clipboard#text <> None
+ method private something_stored = self#markup_stored || self#text_stored
+
+ method canCopy = self#something_selected
+ method canCut = self#text_selected
+ method canDelete = self#text_selected
+ method canPaste = self#something_stored
+ method canPastePattern = self#markup_stored
+
+ method copy () =
+ if self#text_selected
+ then begin
+ MatitaMathView.empty_clipboard ();
+ source_view#buffer#copy_clipboard clipboard;
+ end else
+ MatitaMathView.copy_selection ()
+ method cut () =
+ source_view#buffer#cut_clipboard clipboard;
+ MatitaMathView.empty_clipboard ()
+ method delete () = ignore (source_view#buffer#delete_selection ())
+ method paste () =
+ if MatitaMathView.has_clipboard ()
+ then source_view#buffer#insert (MatitaMathView.paste_clipboard `Term)
+ else source_view#buffer#paste_clipboard clipboard;
+ (MatitaScript.current ())#clean_dirty_lock
+ method pastePattern () =
+ source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern)