Skip to content
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

Merged
merged 1 commit into from
Mar 15, 2024

Conversation

zickgraf
Copy link
Contributor

@zickgraf zickgraf commented Feb 6, 2023

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 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.

@zickgraf
Copy link
Contributor Author

zickgraf commented Feb 6, 2023

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]

@fingolfin
Copy link
Member

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.

@fingolfin
Copy link
Member

Ping @frankluebeck @ChrisJefferson who I think may have an opinion on this.

@frankluebeck
Copy link
Member

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.)

@fingolfin
Copy link
Member

@frankluebeck you have explained alternative solutions for the original problem; but not why you are opposed to this change. What downsides do you perceive?

@frankluebeck
Copy link
Member

@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.

@ChrisJefferson
Copy link
Contributor

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).

@fingolfin
Copy link
Member

@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.

@fingolfin
Copy link
Member

Another compromise (maybe easier to achieve) would of course be to add a user preference for this, as suggested by @ChrisJefferson

@james-d-mitchell
Copy link
Contributor

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".

@fingolfin
Copy link
Member

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.

@james-d-mitchell
Copy link
Contributor

@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!

@zickgraf
Copy link
Contributor Author

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.

@frankluebeck
Copy link
Member

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.

@zickgraf
Copy link
Contributor Author

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 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.

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.

@fingolfin fingolfin closed this Feb 26, 2023
@fingolfin fingolfin reopened this Feb 26, 2023
@zickgraf zickgraf changed the title Do not store duplicate history entries Add user preference "HistoryBackwardSearchUntilChanged" Mar 13, 2023
@zickgraf
Copy link
Contributor Author

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.

@fingolfin
Copy link
Member

Since you didn't like HistoryBackwardSearchUntilChanged: perhaps a variation of HistoryBackwardSkipIdenticalLines or HistoryUpArrowSkipIdenticalLines (though I guess that hardcodes an assumption about key mappings)?

@fingolfin fingolfin added this to the GAP 4.13.0 milestone Feb 12, 2024
Copy link
Member

@fingolfin fingolfin left a 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

@zickgraf zickgraf changed the title Add user preference "HistoryBackwardSearchUntilChanged" Add user preference "HistoryBackwardSearchSkipIdenticalEntries" Feb 13, 2024
@zickgraf
Copy link
Contributor Author

zickgraf commented Feb 13, 2024

@fingolfin thanks a lot for the suggestion, I have now called the preference HistoryBackwardSearchSkipIdenticalEntries and I'm happy with the PR :-)

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.
@zickgraf
Copy link
Contributor Author

The CI failure seems to be an intermittent error.

@fingolfin fingolfin closed this Mar 15, 2024
@fingolfin fingolfin reopened this Mar 15, 2024
@fingolfin fingolfin changed the title Add user preference "HistoryBackwardSearchSkipIdenticalEntries" Add user preference HistoryBackwardSearchSkipIdenticalEntries Mar 15, 2024
@fingolfin fingolfin merged commit a447299 into gap-system:master Mar 15, 2024
44 of 45 checks passed
@fingolfin fingolfin added the release notes: use title For PRs: the title of this PR is suitable for direct use in the release notes label Mar 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
release notes: use title For PRs: the title of this PR is suitable for direct use in the release notes topic: library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants