-
Notifications
You must be signed in to change notification settings - Fork 163
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
Add user preference HistoryBackwardSearchSkipIdenticalEntries
#5366
Conversation
The CI failures are due to network errors:
|
To me this seems fine, I don't think having multiple identical sequential entries in the history (and that's what you are doing) would ever be beneficial to me. I note that Julia also does what this PR proposes, and there I like it. |
Ping @frankluebeck @ChrisJefferson who I think may have an opinion on this. |
I do not support this change. A very useful feature of GAP's history is |
@frankluebeck you have explained alternative solutions for the original problem; but not why you are opposed to this change. What downsides do you perceive? |
@fingolfin: did you miss the second half of my comment? The proposed change breaks the (for me very useful) |
I would like this change personally. It could be added as a user-configurable option (of course then we have to decide the default value for the option). |
@frankluebeck indeed I missed it, ouch. OK, that does make some sense. Perhaps a workable compromise then would be to store all the lines in the history; but pressing the up-arrow would be changed to not just go to the previous entry, but rather if there are multiple identical entries "above", it skips to the first of these. That would give the behavior that @zickgraf @ChrisJefferson and me prefer, while retaining the ability to use ctrl-o for those who use it. |
Another compromise (maybe easier to achieve) would of course be to add a user preference for this, as suggested by @ChrisJefferson |
Something I find useful is being able to go to a line in the history (using the "up" arrow), then hit return, then use the "down" arrow to run through the lines immediately after the previous command. I find this very useful, although I'm not sure that I do this regularly when there are identical lines in the command history (i.e. I'm not sure that I type the same line repeatedly very often, but maybe I do, and I'm just not remembering). I'm not completely sure if this is the same feature that @frankluebeck describes, if it is, then I'd be sad to see this feature removed completely, and would support adding a user preference to control the behaviour. I think the sensible default for this would be the current behaviour which would be "least astonishing". |
I think characterizing "folding identical consecutive lines into a single one" as "completely removing this feature" would be a gross mischaracterization. All it would do is that if there are consecutive identical lines, then in the process you describe, you'd have to remember to press "up" instead of "down" for those lines you want to repeat. But don't get me wrong, I am not saying this to invalidate your concerns or that of Frank, (having to remember to do something else in certain cases is a mental burden and is easy to get it wrong), but let's not exaggerate what is at stake. A user preference would resolve this neatly, I think. |
@fingolfin I didn't characterize:
I only wanted to say that I would be sad if this feature was removed completely! Perhaps I wasn't very clear... It wasn't completely clear to me what the implications of this change would be.
Yes, let's not! |
a4b80e0
to
c1b49f9
Compare
I have now pushed a new suggestion which goes into the direction of the suggestion in #5366 (comment): Searching backwards (e.g. by pressing "up") in history now always ensures that a history entry is selected which actually changes the line (if such an entry exists), with the following reasoning: One usually only presses "up" if one wants something different than the thing currently typed, so we can skip over entries which would not change anything. I think this should only affect other workflows minimally, if at all, and maybe combines the best of all worlds. |
Another general comment: @james-d-mitchell : Yes, your use of Now to the new version of this PR (its title no longer fits with the content!): The idea to skip duplicate lines when the |
True, I agree!
In this setting, are the second and third last line the same? If no, then this PR should not affect this workflow. If yes, then I think my assumption 'One usually only presses "up" if one wants something different than the thing currently typed' is wrong and I should not do this, neither with nor without |
c1b49f9
to
696a908
Compare
I have now put the change behind a new user preference "HistoryBackwardSearchUntilChanged", with the existing behavior staying the default. I'm not 100% happy with the name and the description, so I'm happy for suggestions for improvements. |
696a908
to
723a4bd
Compare
Since you didn't like |
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.
Looks good to me
723a4bd
to
5731e8e
Compare
@fingolfin thanks a lot for the suggestion, I have now called the preference |
When a command is executed multiple times, it is also stored in history multiple times. Setting this option to <K>true</K> skips identical entries when searching backwards in history.
5731e8e
to
fb65564
Compare
The CI failure seems to be an intermittent error. |
HistoryBackwardSearchSkipIdenticalEntries
When debugging loops/recursion using break loops I often find myself in the following situation:
I type some initial command which triggers a loop or recursion with an
Error
inside. Now I typereturn;
until the loop/recursion is a the point I want to debug. I fix something in the code and repeat.Now if I open a new GAP session, the history is full of repeated
return;
entries, so I have to press "arrow up" many times before I reach my original command.This PR adds a user preference "HistoryBackwardSearchSkipIdenticalEntries":
Setting this option to true ensures that during a
backward search a history item is selected which actually changes the
currently displayed line. Note: This does not affect forward searches.
Text for release notes
Add user preference
HistoryBackwardSearchSkipIdenticalEntries
When a command is executed multiple times, it is also stored in history
multiple times. Setting this option to true skips identical entries
when searching backwards in history.