Add an option to keep focus on the model buffer when check with tlc command is invoked #381
Conversation
FedericoPonzi
force-pushed
the
issue-275
branch
3 times, most recently
from
4050eec to
992218b
Compare
|
Issue #275 uses the term "buffer," which I'm unable to interpret in this context. Does it refer to the focus shifting in the direction indicated by the arrow below? If so, the default behavior of the property should be to prevent focus from shifting. This is because the model checker windows don't support keyboard interaction, and the mouse is required to perform any meaningful actions within the view anyway. 
|
package.json
Outdated
| "tlaplus.tlc.modelChecker.preserveEditorFocus": { | ||
| "type": "boolean", | ||
| "scope": "window", | ||
| "default": false, |
| CheckResultViewPanel.currentPanel.panel.reveal(); | ||
| const preserveFocus = vscode.workspace.getConfiguration() | ||
| .get<boolean>('tlaplus.tlc.modelChecker.preserveEditorFocus'); | ||
| CheckResultViewPanel.currentPanel.panel.reveal(undefined, preserveFocus); |
There was a problem hiding this comment.
What happens if the CheckResultView already has focus and the user clicks "Check again"?
Does it shift focus to the editor? In this case, the CheckResultView should retain focus.
There was a problem hiding this comment.
the input to reveal is also called preserveFocus:
* @param preserveFocus When `true`, the webview will not take focus.
Assuming CheckResultViewPanel is in focus and user clicks Check Again:
- if preserveFocus is true, then focus won't change and CheckResultViewPanel stays focused.
- if preserveFocus is false, the focus will shit to the new panel and CheckResultViewPanel will still stay focused
does it answer your question?
…ommand is invoked Signed-off-by: Federico Ponzi <me@fponzi.me>
Signed-off-by: Federico Ponzi <me@fponzi.me>
Yes, that's my interpretation as well, I understood "buffer" in the Emacs sense. The idea of this change is that if your focus remains on the editor, you'll still be able to type after invoking the Check Model with TLC command. I've flip the default to true now. |
Fixes #275.
I've added it as an option (as it would be a "breaking" change) and enabled it by default, but I would be pretty much in favor of get rid of the option and just keep it enabled, but happy to hear other opinions. The option is the most flexible solution.