coqide: Improve find/replace UI

Fixes coq#11024
Frigory33 · Jul 14, 2023 · ee2039c · ee2039c
1 parent f9b0c33
commit ee2039c
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 13 deletions.
diff --git a/ide/coqide/fileOps.ml b/ide/coqide/fileOps.ml
@@ -73,8 +73,8 @@ object(self)
         if not buffer#modified then do_revert f
         else
           let answ = Preferences_ui.question_box
-            ~title:"Modified buffer changed on disk"
-            ~buttons:[ButtonUseStock `REVERT_TO_SAVED;
+            ~title:"Modified buffer changed on disk."
+            ~buttons:[ButtonUseString "Revert from file";
                       ButtonUseString "Overwrite file";
                       ButtonUseString "Disable Auto Revert"]
             ~default:0

diff --git a/ide/coqide/wg_Find.ml b/ide/coqide/wg_Find.ml
@@ -24,12 +24,15 @@ class finder name (view : GText.view) =
   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
+  let find_label = GMisc.label ~text:"Find:"
     ~packing:(replace_box#attach
      (*~xpadding:3 ~ypadding:3*) ~left:0 ~top:1 (*~fill:`X*)) () in
-  let _ = GMisc.label ~text:"Replace:" ~xalign:1.0
+  let replace_label = GMisc.label ~text:"Replace:"
     ~packing:(replace_box#attach
      (* ~xpadding:3 ~ypadding:3*) ~left:0 ~top:2 (*~fill:`X*)) () in
+  let () = List.iter (fun label ->
+      label#set_halign `START; label#set_margin_left 4; label#set_margin_right 4;
+    ) [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
@@ -45,6 +48,8 @@ class finder name (view : GText.view) =
   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
+  let () = List.iter (fun button -> button#set_margin_left 2)
+    [next_button; previous_button; replace_button; replace_all_button] in
 
   object (self)
     val mutable last_found = None
@@ -136,14 +141,17 @@ class finder name (view : GText.view) =
         view#buffer#end_user_action ()
       end
 
-    method private set_not_found () =
-      find_entry#misc#modify_bg [`NORMAL, `NAME "#F7E6E6"];
+    method private set_not_found =
+      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"]
+    method private set_found =
+      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"]
+    method private set_normal =
+      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 =
@@ -157,12 +165,12 @@ class finder name (view : GText.view) =
           self#find_from backward ~wrapped:true view#buffer#end_iter
         else
           let _ = Ideutils.flash_info "String not found" in
-          self#set_not_found ()
+          self#set_not_found
       | Some (start, stop) ->
         let _ = view#buffer#select_range start stop in
         let scroll = `MARK (view#buffer#create_mark stop) in
         let _ = view#scroll_to_mark ~use_align:false scroll in
-        self#set_found ()
+        self#set_found
 
     method find_forward () =
       let starti = view#buffer#get_iter `SEL_BOUND in
@@ -176,6 +184,7 @@ class finder name (view : GText.view) =
 
     method hide () =
       widget#hide;
+      self#set_normal;
       view#coerce#misc#grab_focus ()
 
     method show () =

diff --git a/tools/configure/configure.ml b/tools/configure/configure.ml
@@ -67,7 +67,7 @@ let browser prefs arch =
   | Some b -> b
   | None when arch_is_win32 arch -> "start %s"
   | None when arch = "Darwin" -> "open %s"
-  | _ -> {|xdg-open %s &|}
+  | _ -> "xdg-open %s &"
 
 (** * OCaml programs *)
 module CamlConf = struct