CoqIDE: Improve find/replace UI (margins, icons) #18523
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 ~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 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 ~left:1 ~top:1) () in | ||
| let replace_entry = GEdit.entry ~editable:true | ||
| ~packing:(replace_box#attach ~left:1 ~top:2) () in | ||
| let next_button = GButton.button ~label:"_Next" ~use_mnemonic:true | ||
| ~packing:(replace_box#attach ~left:2 ~top:1) () in | ||
| let previous_button = GButton.button ~label:"_Previous" ~use_mnemonic:true | ||
| ~packing:(replace_box#attach ~left:3 ~top:1) () in | ||
| let replace_button = GButton.button ~label:"_Replace" ~use_mnemonic:true | ||
| ~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 ~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 () = | ||
|
There was a problem hiding this comment. 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. 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 () = | ||
|
There was a problem hiding this comment. 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#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 () = | ||
|
|
||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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_halignbelow, which looks more relevant. If using~xalign:1.0instead, labels are aligned to the right. If using none of them, labels are centered. According to https://docs.gtk.org/gtk3/property.Label.xalign.htmlxalignshould correspond to a “labels size allocation,” but well, how it works is less clear to me thanhalign.