Add history navigation to typewriter input#432
Add history navigation to typewriter input#432414owen wants to merge 1 commit intoleanprover-community:mainfrom
Conversation
This lets the user navigate between previously used lines, in the typewriter input, à la readline. This history persists between levels.
414owen
changed the title
|
Thank you for the PR. This is a nice little feature! Before merging this, I'd want to wait on an outstanding discussion with @TentativeConvert where we were thinking about what sort of input-features (mouse/keyboard/touchpad) interaction would be desirable in the near future. I'd like to first get this big picture and then see how your history integrates into that. |
joneugster
added
feature
| const l = oneLineEditor.onKeyUp((ev) => { | ||
| if (ev.code === "Enter" || ev.code === "NumpadEnter") { | ||
| runCommand() | ||
| } else if (ev.code === "ArrowUp") { |
There was a problem hiding this comment.
I would like ArrowUp and ArrowDown to be available to go through the previous proof states (as having them selected also highlights the corresponding chat messages)
Are there other keys we could use for the history?
There was a problem hiding this comment.
btw, I do plan on having some keyboard shortcut list somewhere, so it's fine if it is a kind of hidden shortcut.
For example: Cmd+H for opening the history, Esc for closing it, and arrows to navigate inside the opened history.
2 participants
This lets the user navigate between previously used lines, in the typewriter input, à la readline.
This history persists between levels.