New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
CoqIDE: Improve find/replace UI (margins, icons) #18523
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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). |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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"]; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Adding the icon and the tooltip are fine, but I would keep the reddish/pink background after an unsuccessful find because some users may prefer the current behavior. GUI detail preferences are subjective. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The part of it which is not subjective is bug #11024 which was caused by the background color. This is the reason to use icons instead. |
||
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"] | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Same thing, I would keep the green. |
||
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 () = | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The xaligns are not needed?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, because I’m using
set_halign
below, which looks more relevant. If using~xalign:1.0
instead, labels are aligned to the right. If using none of them, labels are centered. According to https://docs.gtk.org/gtk3/property.Label.xalign.htmlxalign
should correspond to a “labels size allocation,” but well, how it works is less clear to me thanhalign
.