Skip to content

Commit e2e3a40

Browse files
author
Carolyn Zech
committed
Show coverage info button above harnesses unconditionally
The option to toggle this button on/off in settings didn't work, and I think it's better to just show it to people without hiding it in settings. As long as we print the message that it's unstable (which we do), then there's no risk.
1 parent a2e37a5 commit e2e3a40

File tree

3 files changed

+31
-40
lines changed

3 files changed

+31
-40
lines changed

package.json

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -70,11 +70,6 @@
7070
"type": "boolean",
7171
"default": true
7272
},
73-
"codelens-kani.highlightCoverage": {
74-
"type": "boolean",
75-
"default": false,
76-
"description": "Controls the visibility of the `generate coverage` button by default."
77-
},
7873
"Kani.showOutputWindow": {
7974
"type": "boolean",
8075
"default": false,

src/ui/CodeLensProvider.ts

Lines changed: 30 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -78,40 +78,36 @@ export class CodelensProvider implements vscode.CodeLensProvider {
7878
}
7979
}
8080

81-
// The setting for the coverage code lens needs to be switched on for the mechanism
82-
// to be enabled
83-
if (vscode.workspace.getConfiguration('codelens-kani').get('highlightCoverage', true)) {
84-
// Retrieve harness metadata from the tree-sitter which will be used to place the
85-
// `Get coverage info` code lens button.
86-
const kani_harnesses = await SourceCodeParser.getAttributeFromRustFile(text);
87-
88-
for (const harness of kani_harnesses) {
89-
const harness_name = harness.harnessName;
90-
91-
// If the harness is empty or undefined, skip to the next iteration
92-
if (harness_name === undefined || harness_name === '') {
93-
continue;
94-
}
95-
96-
const startPosition = harness.endPosition;
97-
98-
// This is the metadata that VSCode needs to place the codelens button
99-
const line = document.lineAt(startPosition.row);
100-
const indexOf = line.text.indexOf(harness_name);
101-
const position = new vscode.Position(line.lineNumber, indexOf);
102-
const range = document.getWordRangeAtPosition(position);
103-
104-
const codeCoverageAction = {
105-
title: '$(play) Get coverage info',
106-
tooltip: 'Highlight code with coverage information generated by Kani',
107-
command: 'codelens-kani.highlightCoverage',
108-
arguments: [harness_name],
109-
};
110-
111-
if (range) {
112-
const codeCoverageCodelens = new vscode.CodeLens(range, codeCoverageAction);
113-
this.codeLenses.push(codeCoverageCodelens);
114-
}
81+
// Retrieve harness metadata from the tree-sitter which will be used to place the
82+
// `Get coverage info` code lens button.
83+
const kani_harnesses = await SourceCodeParser.getAttributeFromRustFile(text);
84+
85+
for (const harness of kani_harnesses) {
86+
const harness_name = harness.harnessName;
87+
88+
// If the harness is empty or undefined, skip to the next iteration
89+
if (harness_name === undefined || harness_name === '') {
90+
continue;
91+
}
92+
93+
const startPosition = harness.endPosition;
94+
95+
// This is the metadata that VSCode needs to place the codelens button
96+
const line = document.lineAt(startPosition.row);
97+
const indexOf = line.text.indexOf(harness_name);
98+
const position = new vscode.Position(line.lineNumber, indexOf);
99+
const range = document.getWordRangeAtPosition(position);
100+
101+
const codeCoverageAction = {
102+
title: '$(play) Get coverage info',
103+
tooltip: 'Highlight code with coverage information generated by Kani',
104+
command: 'codelens-kani.highlightCoverage',
105+
arguments: [harness_name],
106+
};
107+
108+
if (range) {
109+
const codeCoverageCodelens = new vscode.CodeLens(range, codeCoverageAction);
110+
this.codeLenses.push(codeCoverageCodelens);
115111
}
116112
}
117113
return this.codeLenses;

src/ui/coverage/coverageInfo.ts

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ enum CoverageStatus {
3232
None = 'NONE',
3333
}
3434

35-
const warningMessage = `Line coverage is an unstable feature.`;
35+
const warningMessage = `Source-based coverage is an unstable feature.`;
3636

3737
// Callback function for the coverage code lens action
3838
export async function runCodeCoverageAction(

0 commit comments

Comments
 (0)