gap
gap copied to clipboard
gap-system
Add user preference "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 type return; 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 <K>true</K> 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 <K>true</K> skips identical entries when searching backwards in history.
The CI failures are due to network errors:
Err:15 http://azure.archive.ubuntu.com/ubuntu jammy/universe amd64 texlive-base all 2021.20220204-1
Connection failed [IP: 20.106.104.242 80]
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. You can easily avoid the large number of up arrows by typing the first (few) character(s) of the command you are looking for.
A very useful feature of GAP's history is Ctrl-o which sends the current line and fills the input with the following line in the history. This is very useful to repeat a sequence of commands (optionally slightly edited), and I often use it. But for this to work smoothly the history should store exactly all input lines. (And it happens that I call the same line two or more times.)
@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) Ctrl-o feature of GAP's history mechanism.
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".
sad to see this feature removed completely
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:
"folding identical consecutive lines into a single one" as "completely removing this feature"
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.
but let's not exaggerate what is at stake.
Yes, let's not!
I have now pushed a new suggestion which goes into the direction of the suggestion in https://github.com/gap-system/gap/pull/5366#issuecomment-1425405030: 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: The GAP history contains a precise record of all input lines. This feature should not be changed. It is not only useful for some command line editing functions. (E.g., I often print the lines in the history to reuse (a polished version) of my interactive input.
@james-d-mitchell : Yes, your use of <Enter> <Down> is connected with my previous comment. Actually, <Ctrl-o> just combines <Enter> <Down> in one keystroke - very useful to repeat a sequence of input lines.
Now to the new version of this PR (its title no longer fits with the content!): The idea to skip duplicate lines when the <UP> key is used several times, sounds good to me. But only when used with no start characters. In interactive work, in the context I described in my first comment, I often type some characters as start and want to get back to the second or third last line with this beginning to repeat a sequence of input lines starting there.
The GAP history contains a precise record of all input lines. This feature should not be changed. It is not only useful for some command line editing functions. (E.g., I often print the lines in the history to reuse (a polished version) of my interactive input.
True, I agree!
In interactive work, in the context I described in my first comment, I often type some characters as
startand want to get back to the second or third last line with this beginning to repeat a sequence of input lines starting there.
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 start characters.
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.
Since you didn't like HistoryBackwardSearchUntilChanged: perhaps a variation of HistoryBackwardSkipIdenticalLines or HistoryUpArrowSkipIdenticalLines (though I guess that hardcodes an assumption about key mappings)?
@fingolfin thanks a lot for the suggestion, I have now called the preference HistoryBackwardSearchSkipIdenticalEntries and I'm happy with the PR :-)