coqide: Add “Select All” item in the Edit menu

Fixes coq#16141
Frigory33 · Jul 14, 2023 · f9b0c33 · f9b0c33
1 parent 6c052d6
commit f9b0c33
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 0 deletions.
diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml
@@ -1445,6 +1445,8 @@ let build_ui () =
       ~callback:(cb_on_current_term (fun t -> t.script#undo ()));
     item "Redo" ~accel:"<Primary>y" ~stock:`REDO
       ~callback:(cb_on_current_term (fun t -> t.script#redo ()));
+    item "Select All" ~accel:"<Primary>a" ~stock:`SELECT_ALL
+      ~callback:(cb_on_current_term (fun t -> t.script#select_all ()));
     item "Cut" ~stock:`CUT
       ~callback:(fun _ -> emit_to_focus w GtkText.View.S.cut_clipboard);
     item "Copy" ~stock:`COPY

diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml
@@ -52,6 +52,7 @@ let init () =
     <menuitem action='Undo' />
     <menuitem action='Redo' />
     <separator />
+    <menuitem action='Select All' />
     <menuitem action='Cut' />
     <menuitem action='Copy' />
     <menuitem action='Paste' />

diff --git a/ide/coqide/wg_ScriptView.ml b/ide/coqide/wg_ScriptView.ml
@@ -361,6 +361,9 @@ object (self)
     } in
     Gobject.set prop obj show
 
+  method select_all () =
+    self#buffer#select_range self#buffer#start_iter self#buffer#end_iter
+
   method comment () =
     let rec get_line_start iter =
       if iter#starts_line then iter

diff --git a/ide/coqide/wg_ScriptView.mli b/ide/coqide/wg_ScriptView.mli
@@ -24,6 +24,7 @@ object
   method set_right_margin_position : int -> unit
   method show_right_margin : bool
   method set_show_right_margin : bool -> unit
+  method select_all : unit -> unit
   method comment : unit -> unit
   method uncomment : unit -> unit
   method apply_unicode_binding : unit -> unit