From 4f04bf7d4032d301ce723fce357a27f92f003893 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 9 Dec 2005 13:00:47 +0000 Subject: [PATCH] implemented copy/cut/paste/delete/pastePattern --- helm/matita/matita.glade | 42 ++++---- helm/matita/matita.ml | 4 +- helm/matita/matitaGui.ml | 114 +++++++++++++++------ helm/matita/matitaGuiTypes.mli | 22 ++++- helm/matita/matitaMathView.ml | 174 +++++++++++++++++++++++---------- helm/matita/matitaMathView.mli | 15 ++- 6 files changed, 267 insertions(+), 104 deletions(-) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 6ddd786b9..436dd7b26 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -877,7 +877,7 @@ - + True gtk-new 1 @@ -898,7 +898,7 @@ - + True gtk-open 1 @@ -919,7 +919,7 @@ - + True gtk-save 1 @@ -940,7 +940,7 @@ - + True gtk-save-as 1 @@ -961,7 +961,7 @@ - + True gtk-execute 1 @@ -988,7 +988,7 @@ - + True gtk-quit 1 @@ -1023,7 +1023,7 @@ - + True gtk-undo 1 @@ -1045,7 +1045,7 @@ - + True gtk-redo 1 @@ -1072,7 +1072,7 @@ - + True gtk-cut 1 @@ -1093,7 +1093,7 @@ - + True gtk-copy 1 @@ -1114,7 +1114,7 @@ - + True gtk-paste 1 @@ -1127,6 +1127,14 @@ + + + True + Paste as pattern + True + + + True @@ -1134,7 +1142,7 @@ True - + True gtk-delete 1 @@ -1175,7 +1183,7 @@ - + True gtk-find-and-replace 1 @@ -1344,7 +1352,7 @@ - + True gtk-zoom-in 1 @@ -1366,7 +1374,7 @@ - + True gtk-zoom-out 1 @@ -1387,7 +1395,7 @@ - + True gtk-zoom-100 1 @@ -1439,7 +1447,7 @@ True - + True gtk-about 1 diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index efaaa5707..1f49c1ac5 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -117,9 +117,9 @@ let _ = List.iter (fun (u,_,_) -> prerr_endline (UriManager.string_of_uri u)) (CicEnvironment.list_obj ())); - addDebugItem "print selections" (fun () -> +(* addDebugItem "print selections" (fun () -> let cicMathView = MatitaMathView.cicMathView_instance () in - List.iter HLog.debug (cicMathView#string_of_selections)); + List.iter HLog.debug (cicMathView#string_of_selections)); *) addDebugItem "dump script status" script#dump; addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ -> Helm_registry.save_to "./foo.conf.xml"); diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 6308eab86..5aa3d59e9 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -110,6 +110,16 @@ let ask_unsaved parent = "Do you want to save the script before continuing?") () +(** Selection handling + * Two clipboards are used: "clipboard" and "primary". + * "primary" is used by X, when you hit the middle button mouse is content is + * pasted between applications. In Matita this selection always contain the + * textual version of the selected term. + * "clipboard" is used inside Matita only and support ATM two different targets: + * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may + * be added + *) + class gui () = (* creation order _is_ relevant for windows placement *) let main = new mainWin () in @@ -143,6 +153,8 @@ class gui () = val mutable font_size = default_font_size val mutable next_devel_must_contain = None val mutable next_ligatures = [] + val clipboard = GData.clipboard Gdk.Atom.clipboard + val primary = GData.clipboard Gdk.Atom.primary initializer (* glade's check widgets *) @@ -310,8 +322,32 @@ class gui () = let undoMenuItem, redoMenuItem = match menuItems with [undo;redo;sep1;cut;copy;paste;delete;sep2; - selectall;sep3;inputmethod;insertunicodecharacter] -> undo,redo + selectall;sep3;inputmethod;insertunicodecharacter] -> + List.iter menu#remove [ copy; cut; delete; paste ]; + undo,redo | _ -> assert false in + let add_menu_item = + let i = ref 2 in (* last occupied position *) + fun ?label ?stock () -> + incr i; + GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i) + () + in + let copy = add_menu_item ~stock:`COPY () in + let cut = add_menu_item ~stock:`CUT () in + let delete = add_menu_item ~stock:`DELETE () in + let paste = add_menu_item ~stock:`PASTE () in + let paste_pattern = add_menu_item ~label:"Paste as pattern" () in + copy#misc#set_sensitive self#canCopy; + cut#misc#set_sensitive self#canCut; + delete#misc#set_sensitive self#canDelete; + paste#misc#set_sensitive self#canPaste; + paste_pattern#misc#set_sensitive self#canPastePattern; + connect_menu_item copy self#copy; + connect_menu_item cut self#cut; + connect_menu_item delete self#delete; + connect_menu_item paste self#paste; + connect_menu_item paste_pattern self#pastePattern; let new_undoMenuItem = GMenu.image_menu_item ~image:(GMisc.image ~stock:`UNDO ()) @@ -332,35 +368,18 @@ class gui () = (redoMenuItem#misc#get_flag `SENSITIVE); menu#remove (redoMenuItem :> GMenu.menu_item); connect_menu_item new_redoMenuItem safe_redo)); - let clipboard = GData.clipboard Gdk.Atom.clipboard in - let text_selected () = - (source_buffer#get_iter_at_mark `INSERT)#compare - (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0 - in - let markup_selected () = MatitaMathView.get_selections () <> None in + connect_menu_item main#editMenu (fun () -> - let text_selected = text_selected () in - let markup_selected = markup_selected () in - let something_selected = text_selected || markup_selected in - main#cutMenuItem#misc#set_sensitive text_selected; - main#copyMenuItem#misc#set_sensitive something_selected; - main#deleteMenuItem#misc#set_sensitive text_selected; - main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None)); - connect_menu_item main#cutMenuItem (fun () -> - source_view#buffer#cut_clipboard clipboard); - connect_menu_item main#copyMenuItem (fun () -> - if text_selected () then - source_view#buffer#copy_clipboard clipboard - else if markup_selected () then - match MatitaMathView.get_selections () with - | None - | Some [] -> () - | Some (s :: _) -> clipboard#set_text s); - connect_menu_item main#pasteMenuItem (fun () -> - source_view#buffer#paste_clipboard clipboard; - (MatitaScript.current ())#clean_dirty_lock); - connect_menu_item main#deleteMenuItem (fun () -> - ignore (source_view#buffer#delete_selection ())); + main#copyMenuItem#misc#set_sensitive self#canCopy; + main#cutMenuItem#misc#set_sensitive self#canCut; + main#deleteMenuItem#misc#set_sensitive self#canDelete; + main#pasteMenuItem#misc#set_sensitive self#canPaste; + main#pastePatternMenuItem#misc#set_sensitive self#canPastePattern); + connect_menu_item main#copyMenuItem self#copy; + connect_menu_item main#cutMenuItem self#cut; + connect_menu_item main#deleteMenuItem self#delete; + connect_menu_item main#pasteMenuItem self#paste; + connect_menu_item main#pastePatternMenuItem self#pastePattern; connect_menu_item main#selectAllMenuItem (fun () -> source_buffer#move_mark `INSERT source_buffer#start_iter; source_buffer#move_mark `SEL_BOUND source_buffer#end_iter); @@ -801,6 +820,43 @@ class gui () = MatitaMathView.reset_font_size (); MatitaMathView.update_font_sizes ()); MatitaMathView.reset_font_size (); + + (** 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) method private nextLigature () = let iter = source_buffer#get_iter_at_mark `INSERT in diff --git a/helm/matita/matitaGuiTypes.mli b/helm/matita/matitaGuiTypes.mli index efb704579..c68bbc28e 100644 --- a/helm/matita/matitaGuiTypes.mli +++ b/helm/matita/matitaGuiTypes.mli @@ -66,6 +66,20 @@ object method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog + (** {2 Selections / clipboards handling} *) + + method canCopy: bool + method canCut: bool + method canDelete: bool + method canPaste: bool + method canPastePattern: bool + + method copy: unit -> unit + method cut: unit -> unit + method delete: unit -> unit + method paste: unit -> unit + method pastePattern: unit -> unit + (** {2 Utility methods} *) (** ask the used to choose a file with the file chooser @@ -86,6 +100,8 @@ object method resetFontSize: unit -> unit end +type paste_kind = [ `Term | `Pattern ] + (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions * are handled internally. Hyperlinks are handled by calling an user provided * callback *) @@ -96,8 +112,10 @@ object (** set hyperlink callback. None disable hyperlink handling *) method set_href_callback: (string -> unit) option -> unit - method string_of_selections: string list - method string_of_selection: string option (* last selected node *) + method has_selection: bool + + (** @raise Failure "no selection" *) + method strings_of_selection: (paste_kind * string) list method update_font_size: unit end diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index b637eb8dc..e949020d9 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -27,6 +27,7 @@ open Printf open GrafiteTypes open MatitaGtkMisc +open MatitaGuiTypes module Stack = Continuationals.Stack @@ -161,12 +162,20 @@ object (self) val mutable selection_changed = false method private selection_get_cb ctxt ~info ~time = - (match self#get_selections with + match self#get_selections with | [] -> () - | node :: _ -> ctxt#return (self#string_of_node node)) + | node :: _ -> +(* eprintf "getting selection with target %s\n%!" ctxt#target; *) + (match ctxt#target with + | "PATTERN" -> + ctxt#return (self#string_of_node ~paste_kind:`Pattern node) + | "TERM" | _ -> + ctxt#return (self#string_of_node ~paste_kind:`Term node)) method private selection_clear_cb sel_event = +(* eprintf "selection clear\n%!"; *) self#remove_selections; + (GData.clipboard Gdk.Atom.clipboard)#clear (); false method private button_press_cb gdk_button = @@ -180,20 +189,18 @@ object (self) false method private popup_contextual_menu time = - match self#string_of_selection with - | None -> () - | Some s -> - let clipboard = GData.clipboard Gdk.Atom.clipboard in - let menu = GMenu.menu () in - let copy_menu_item = - GMenu.image_menu_item - ~label:"_Copy" ~stock:`COPY ~packing:menu#append () - in - connect_menu_item copy_menu_item (fun () -> clipboard#set_text s); - menu#popup ~button:right_button ~time + let clipboard = GData.clipboard Gdk.Atom.clipboard in + let menu = GMenu.menu () in + let copy_menu_item = + GMenu.image_menu_item + ~label:"_Copy" ~stock:`COPY ~packing:menu#append () + in + let gui = get_gui () in + copy_menu_item#misc#set_sensitive gui#canCopy; + connect_menu_item copy_menu_item gui#copy; + menu#popup ~button:right_button ~time method private button_release_cb gdk_button = - let clipboard = GData.clipboard Gdk.Atom.primary in if GdkEvent.Button.button gdk_button = left_button then begin let button_release_x = GdkEvent.Button.x gdk_button in let button_release_y = GdkEvent.Button.y gdk_button in @@ -240,13 +247,11 @@ object (self) menu#popup ~button ~time) method private choose_selection_cb gdome_elt = - let (gui: MatitaGuiTypes.gui) = get_gui () in - let clipboard = GData.clipboard Gdk.Atom.primary in let set_selection elt = + let misc = self#coerce#misc in self#set_selection (Some elt); - self#coerce#misc#add_selection_target - ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary; - ignore (self#coerce#misc#grab_selection Gdk.Atom.primary) + misc#add_selection_target ~target:"STRING" Gdk.Atom.primary; + ignore (misc#grab_selection Gdk.Atom.primary); in let rec aux elt = if (elt#getAttributeNS ~namespaceURI:helm_ns @@ -296,12 +301,12 @@ object (self) in (try Hashtbl.find ids_to_terms id with Not_found -> assert false) - method private string_of_node node = + method private string_of_node ~(paste_kind:paste_kind) node = if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds - then self#string_of_id_node node + then self#string_of_id_node ~paste_kind node else string_of_dom_node node - method private string_of_id_node node = + method private string_of_id_node ~(paste_kind:paste_kind) node = let get_id (node: Gdome.element) = let xref_attr = node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds @@ -316,12 +321,6 @@ object (self) else [] in -(* TODO: code for patterns - let conclusion = (MatitaScript.instance ())#proofConclusion in - let conclusion_pattern = - ProofEngineHelpers.pattern_of ~term:conclusion cic_terms - in -*) let string_of_cic_sequent cic_sequent = let _, (acic_sequent, _, _, ids_to_inner_sorts, _) = Cic2acic.asequent_of_sequent metasenv cic_sequent @@ -345,29 +344,78 @@ object (self) info, (~-1, [], t) | None -> assert false in + let paste_as_pattern_sequent term unsh_sequent = + match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with + | [context, _] -> + (let context_len = List.length context in + let _, unsh_context, conclusion = unsh_sequent in + try + (match + List.nth unsh_context (List.length unsh_context - context_len - 1) + with + | None -> assert false (* can't select a restricted hyp *) + | Some (name, Cic.Decl ty) -> + let pattern = + ProofEngineHelpers.pattern_of ~term:ty [term] + in + HLog.debug (CicPp.ppname name ^ ":" ^ CicPp.ppterm pattern); + ~-1, [], pattern + | Some (name, Cic.Def (bo, _)) -> + let pattern = + ProofEngineHelpers.pattern_of ~term:bo [term] + in + HLog.debug (CicPp.ppname name ^ ":=" ^ CicPp.ppterm pattern); + ~-1, [], pattern) + with Failure _ | Invalid_argument _ -> + let pattern = + ProofEngineHelpers.pattern_of ~term:conclusion [term] + in + HLog.debug ("\\vdash " ^ CicPp.ppterm pattern); + ~-1, [], pattern) + | _ -> assert false (* since it uses physical equality *) + in + let paste_as_term_sequent term unsh_sequent = + let context' = + match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with + | [context,_] -> context + | _ -> assert false (* since it uses physical equality *) + in + ~-1, context', term + in let cic_sequent = match self#get_term_by_id cic_info id with | `Term t -> - let context' = - match ProofEngineHelpers.locate_in_conjecture t unsh_sequent with - [context,_] -> context - | _ -> -(* prerr_endline (sprintf "%d\nt=%s\ncontext=%s" - (List.length l) (CicPp.ppterm t) (CicPp.ppcontext context)); *) - assert false (* since it uses physical equality *) - in - ~-1, context', t + (match paste_kind with + | `Term -> paste_as_term_sequent t unsh_sequent + | `Pattern -> paste_as_pattern_sequent t unsh_sequent) | `Hyp context -> ~-1, context, Cic.Rel 1 in string_of_cic_sequent cic_sequent - method string_of_selections = - List.map self#string_of_node (List.rev self#get_selections) - - method string_of_selection = + method private string_of_selection ~(paste_kind:paste_kind) = match self#get_selections with | [] -> None - | node :: _ -> Some (self#string_of_node node) + | node :: _ -> Some (self#string_of_node ~paste_kind node) + + method has_selection = self#get_selections <> [] + + (** @return an associative list format -> string with all possible selection + * formats. Rationale: in order to convert the selection to TERM or PATTERN + * format we need the sequent, the metasenv, ... keeping all of them in a + * closure would be more expensive than keeping their already converted + * forms *) + method strings_of_selection = + try + let misc = self#coerce#misc in + List.iter + (fun target -> misc#add_selection_target ~target Gdk.Atom.clipboard) + [ "TERM"; "PATTERN"; "STRING" ]; + ignore (misc#grab_selection Gdk.Atom.clipboard); + List.map + (fun paste_kind -> + paste_kind, HExtlib.unopt (self#string_of_selection ~paste_kind)) + [ `Term; `Pattern ] + with Failure _ -> failwith "no selection" end @@ -465,6 +513,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = notebook#append_page logo_with_qed method reset = + cicMathView#remove_selections; (match scrolledWin with | Some w -> (* removing page from the notebook will destroy all contained widget, @@ -487,7 +536,6 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#script#setGoal ~-1; method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } = - let sequents_no = List.length metasenv in _metasenv <- metasenv; pages <- 0; let win goal_switch = @@ -621,7 +669,6 @@ type term_source = class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) () = - let term_RE = Pcre.regexp "^term:(.*)" in let whelp_RE = Pcre.regexp "^\\s*whelp" in let uri_RE = Pcre.regexp @@ -629,8 +676,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in - let trailing_slash_RE = Pcre.regexp "/$" in - let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in @@ -969,7 +1014,7 @@ let mathViewer () = end let refresh_all_browsers () = - List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers + List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers let update_font_sizes () = List.iter (fun b -> b#updateFontSize) !cicBrowsers; @@ -979,7 +1024,38 @@ let get_math_views () = ((cicMathView_instance ()) :> MatitaGuiTypes.clickableMathView) :: (List.map (fun b -> b#mathView) !cicBrowsers) -let get_selections () = +let find_selection_owner () = + let rec aux = + function + | [] -> raise Not_found + | mv :: tl -> + (match mv#get_selections with + | [] -> aux tl + | sel :: _ -> mv) + in + aux (get_math_views ()) + +let has_selection () = + try ignore (find_selection_owner ()); true + with Not_found -> false + +let math_view_clipboard = ref None (* associative list target -> string *) +let has_clipboard () = !math_view_clipboard <> None +let empty_clipboard () = math_view_clipboard := None + +let copy_selection () = + try + math_view_clipboard := + Some ((find_selection_owner ())#strings_of_selection) + with Not_found -> failwith "no selection" + +let paste_clipboard paste_kind = + match !math_view_clipboard with + | None -> failwith "empty clipboard" + | Some cb -> + (try List.assoc paste_kind cb with Not_found -> assert false) + +(* let get_selections () = if (MatitaScript.current ())#onGoingProof () then let rec aux = function @@ -994,5 +1070,5 @@ let get_selections () = None let reset_selections () = - List.iter (fun mv -> mv#remove_selections) (get_math_views ()) + List.iter (fun mv -> mv#remove_selections) (get_math_views ()) *) diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index f5acf6349..ea0c077d8 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -61,13 +61,18 @@ val reset_font_size: unit -> unit val refresh_all_browsers: unit -> unit (** act on all cicBrowsers *) val update_font_sizes: unit -> unit - (** {3 selection handling} *) + (** {3 Clipboard & Selection handling} *) - (* @return the selections of a (unspecified) math viewer *) -val get_selections: unit -> string list option +val has_selection: unit -> bool - (* remove the selections of all math viewers *) -val reset_selections: unit -> unit + (** fills the clipboard with the current selection + * @raise Failure "no selection" *) +val copy_selection: unit -> unit +val has_clipboard: unit -> bool (** clipboard is not empty *) +val empty_clipboard: unit -> unit (** empty the clipboard *) + + (** @raise Failure "empty clipboard" *) +val paste_clipboard: MatitaGuiTypes.paste_kind -> string (** {2 Singleton instances} *) -- 2.39.2