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

Show model/spec name in VSCode status bar #285

Closed
lemmy opened this issue Apr 25, 2023 · 0 comments
Closed

Show model/spec name in VSCode status bar #285

lemmy opened this issue Apr 25, 2023 · 0 comments
Assignees
Labels
enhancement New feature or request good first issue Good for newcomers
Milestone

Comments

@lemmy
Copy link
Member

lemmy commented Apr 25, 2023

During the execution of TLC, you'll notice a rotating wheel adjacent to the "TLC" label located in the status bar. Additionally, the present specification and/or module's name should also be displayed.

function updateStatusBarItem(active: boolean) {
statusBarItem.text = 'TLC' + (active ? ' $(gear~spin)' : '');
statusBarItem.tooltip = 'TLA+ model checking' + (active ? ' is running' : ' result');
statusBarItem.command = CMD_CHECK_MODEL_DISPLAY;
statusBarItem.show();
vscode.commands.executeCommand('setContext', CTX_TLC_RUNNING, active);
}

@lemmy lemmy added enhancement New feature or request good first issue Good for newcomers labels Apr 25, 2023
lemmy added a commit that referenced this issue Apr 25, 2023
Implements Github issue #285
#285

[Feature]
@lemmy lemmy added this to the v1.7.0 milestone Apr 25, 2023
@lemmy lemmy self-assigned this Apr 25, 2023
@lemmy lemmy closed this as completed Apr 25, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request good first issue Good for newcomers
Development

No branches or pull requests

1 participant