From 014fd11a9ad0eb5d0b553253bb56e98c79c0740c Mon Sep 17 00:00:00 2001
From: Sylvain Chiron <chironsylvain@orange.fr>
Date: Sat, 1 Apr 2023 15:04:39 +0200
Subject: [PATCH] coqide: Improve find/replace UI (margins, icons)

Fixes #11024
---
 doc/changelog/10-coqide/18523-coqide.rst |  5 +++
 ide/coqide/wg_Find.ml                    | 47 +++++++++++++-----------
 2 files changed, 31 insertions(+), 21 deletions(-)
 create mode 100644 doc/changelog/10-coqide/18523-coqide.rst

diff --git a/doc/changelog/10-coqide/18523-coqide.rst b/doc/changelog/10-coqide/18523-coqide.rst
new file mode 100644
index 000000000000..bf95e925a4a3
--- /dev/null
+++ b/doc/changelog/10-coqide/18523-coqide.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Find/replace UI was improved: margins, icons for found/not found
+  (`#18523 <https://github.com/coq/coq/pull/18523>`_,
+  fixes `#11024 <https://github.com/coq/coq/issues/11024>`_,
+  by Sylvain Chiron).
diff --git a/ide/coqide/wg_Find.ml b/ide/coqide/wg_Find.ml
index 3fbf9288e6c0..edf92611c8ab 100644
--- a/ide/coqide/wg_Find.ml
+++ b/ide/coqide/wg_Find.ml
@@ -14,37 +14,38 @@ class finder name (view : GText.view) =
 
   let widget = Wg_Detachable.detachable
     ~title:(Printf.sprintf "Find & Replace (%s)" name) () in
-  let replace_box = GPack.grid (* ~columns:4 ~rows:2 *) ~col_homogeneous:false ~row_homogeneous:false
-    ~packing:widget#add () in
-  let hb = GPack.hbox ~packing:(replace_box#attach
-      ~left:1 ~top:0 (*~expand:`X ~fill:`X*)) () in
+  let replace_box = GPack.grid ~col_homogeneous:false ~row_homogeneous:false
+    ~row_spacings:2 ~col_spacings:2 ~packing:widget#add () in
+  let () = replace_box#set_margin 2 in
+  let hb = GPack.hbox ~packing:(replace_box#attach ~left:1 ~top:0) () in
   let use_regex =
     GButton.check_button ~label:"Regular expression"
       ~packing:(hb#pack ~expand:false ~fill:true ~padding:3) () in
   let use_nocase =
     GButton.check_button ~label:"Case insensitive"
       ~packing:(hb#pack ~expand:false ~fill:true ~padding:3) () in
-  let _ = GMisc.label ~text:"Find:" ~xalign:1.0
-    ~packing:(replace_box#attach
-     (*~xpadding:3 ~ypadding:3*) ~left:0 ~top:1 (*~fill:`X*)) () in
-  let _ = GMisc.label ~text:"Replace:" ~xalign:1.0
-    ~packing:(replace_box#attach
-     (* ~xpadding:3 ~ypadding:3*) ~left:0 ~top:2 (*~fill:`X*)) () in
+  let find_label = GMisc.label ~text:"Find:"
+    ~packing:(replace_box#attach ~left:0 ~top:1) () in
+  let replace_label = GMisc.label ~text:"Replace with:"
+    ~packing:(replace_box#attach ~left:0 ~top:2) () in
+  let () = List.iter (fun label ->
+      label#set_halign `START;
+      label#set_margin_left 2;
+      label#set_margin_right 2;
+    ) [find_label; replace_label] in
   let find_entry = GEdit.entry ~editable:true
-    ~packing:(replace_box#attach
-      (*~xpadding:3 ~ypadding:3*) ~left:1 ~top:1 (*~expand:`X ~fill:`X*)) () in
+    ~packing:(replace_box#attach ~left:1 ~top:1) () in
   let replace_entry = GEdit.entry ~editable:true
-    ~packing:(replace_box#attach
-      (*~xpadding:3 ~ypadding:3*) ~left:1 ~top:2 (*~expand:`X ~fill:`X*)) () in
+    ~packing:(replace_box#attach ~left:1 ~top:2) () in
   let next_button = GButton.button ~label:"_Next" ~use_mnemonic:true
-    ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:2 ~top:1) () in
+    ~packing:(replace_box#attach ~left:2 ~top:1) () in
   let previous_button = GButton.button ~label:"_Previous" ~use_mnemonic:true
-    ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:3 ~top:1) () in
+    ~packing:(replace_box#attach ~left:3 ~top:1) () in
   let replace_button = GButton.button ~label:"_Replace" ~use_mnemonic:true
-    ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:2 ~top:2) () in
+    ~packing:(replace_box#attach ~left:2 ~top:2) () in
   let replace_all_button =
     GButton.button ~label:"Replace _All" ~use_mnemonic:true
-      ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:3 ~top:2) () in
+      ~packing:(replace_box#attach ~left:3 ~top:2) () in
 
   object (self)
     val mutable last_found = None
@@ -137,13 +138,16 @@ class finder name (view : GText.view) =
       end
 
     method private set_not_found () =
-      find_entry#misc#modify_bg [`NORMAL, `NAME "#F7E6E6"];
+      find_entry#set_secondary_icon_stock `DELETE;
+      find_entry#set_secondary_icon_tooltip_text "String not found";
 
     method private set_found () =
-      find_entry#misc#modify_bg [`NORMAL, `NAME "#BAF9CE"]
+      find_entry#set_secondary_icon_stock `FIND;
+      find_entry#set_secondary_icon_tooltip_text "String found";
 
     method private set_normal () =
-      find_entry#misc#modify_bg [`NORMAL, `NAME "white"]
+      find_entry#set_secondary_icon_stock (`STOCK "");
+      find_entry#set_secondary_icon_tooltip_text "";
 
     method private find_from backward ?(wrapped=false) (starti : GText.iter) =
       let found =
@@ -176,6 +180,7 @@ class finder name (view : GText.view) =
 
     method hide () =
       widget#hide;
+      self#set_normal ();
       view#coerce#misc#grab_focus ()
 
     method show () =