CoqIDE: Improve find/replace UI (margins, icons) #18523
Conversation
coqbot-app
bot
added
the
needs: full CI
Frigory33
force-pushed
the
coqide-findreplace
branch
from
e38accd
to
0ca5639
Compare
Frigory33
force-pushed
the
coqide-findreplace
branch
2 times, most recently
from
dc85911
to
2808666
Compare
|
These are the differences I see between master and this PR. Perhaps you want to add a little vertical space between the Find and "Replace with" lines and below "Replace with"?
FWIW the Find/Can't find icons don't show up until you've done a search or replace:
|
There was a problem hiding this comment.
The changes here are minor. I think they won't make any significant difference in usability for users. Given that we have limited resources to make and review changes and the many things that deserve to be improved, I hope you'll focus on more impactful changes in the future.
| @@ -137,13 +139,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.
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.
|
|
||
| method private set_found () = | ||
| find_entry#misc#modify_bg [`NORMAL, `NAME "#BAF9CE"] |
There was a problem hiding this comment.
Same thing, I would keep the green.
| 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 |
There was a problem hiding this comment.
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.html xalign should correspond to a “labels size allocation,” but well, how it works is less clear to me than halign.
|
With my GTK theme, the vertical spacing was quite okay: |
Frigory33
force-pushed
the
coqide-findreplace
branch
from
2808666
to
014fd11
Compare
|
I added row and col spacing in the grid, and margin around the grid: |
jfehrle
removed
the
needs: full CI
|
@coqbot: run full ci |
jfehrle
added
the
part: CoqIDE
|
@coqbot: merge now |
|
@jfehrle: You cannot merge this PR because:
|
jfehrle
added
the
kind: usability
|
@coqbot: merge now |
|
By the way, would it be easy to add a way to remove the search/replace window? Currently, the way I use is to detach and delete the detached window, but a one-click way would be convenient. |
Just press Escape. |
Wonderful, I learn new things every day! |
Fixes #11024