diff --git a/package.json b/package.json index dc3ce0a4..d2eabb3c 100644 --- a/package.json +++ b/package.json @@ -56,6 +56,11 @@ "command": "dafny.run", "group": "7_Dafny@7" }, + { + "when": "editorTextFocus && editorLangId == dafny", + "command": "dafny.test", + "group": "7_Dafny@8" + }, { "when": "editorTextFocus && editorLangId == dafny && dafny.counterexampleMenu.CanShowCounterExample", "command": "dafny.showCounterexample", @@ -86,6 +91,12 @@ "mac": "f5", "when": "editorTextFocus && editorLangId == dafny" }, + { + "command": "dafny.test", + "key": "shift+f5", + "mac": "⇧f5", + "when": "editorTextFocus && editorLangId == dafny" + }, { "command": "dafny.buildCustomArgs", "key": "f6", @@ -267,6 +278,10 @@ "command": "dafny.buildCustomArgs", "title": "Dafny: Build with Custom Arguments" }, + { + "command": "dafny.test", + "title": "Dafny: Test" + }, { "command": "dafny.run", "title": "Dafny: Run" diff --git a/src/commands.ts b/src/commands.ts index 73d33007..3b5dafa4 100644 --- a/src/commands.ts +++ b/src/commands.ts @@ -2,6 +2,7 @@ export namespace DafnyCommands { export const Build = 'dafny.build'; export const BuildCustomArgs = 'dafny.buildCustomArgs'; export const Run = 'dafny.run'; + export const Test = 'dafny.test'; export const ShowCounterexample = 'dafny.showCounterexample'; export const HideCounterexample = 'dafny.hideCounterexample'; export const CopyCounterexamples = 'dafny.copyCounterexamples'; diff --git a/src/ui/compileCommands.ts b/src/ui/compileCommands.ts index 402fb934..0be408d0 100644 --- a/src/ui/compileCommands.ts +++ b/src/ui/compileCommands.ts @@ -11,18 +11,32 @@ import { Messages } from './messages'; const OutputPathArg = '--output'; +enum CommandType { + Build, + Run, + Test +} + export default class CompileCommands { public static createAndRegister(installer: DafnyInstaller): CompileCommands { installer.context.subscriptions.push( - commands.registerCommand(DafnyCommands.Build, () => buildOrRun(installer, false, false)), - commands.registerCommand(DafnyCommands.BuildCustomArgs, () => buildOrRun(installer, true, false)), - commands.registerCommand(DafnyCommands.Run, () => buildOrRun(installer, false, true)) + commands.registerCommand(DafnyCommands.Build, () => + buildRunOrTest(installer, CommandType.Build, false)), + commands.registerCommand(DafnyCommands.BuildCustomArgs, () => + buildRunOrTest(installer, CommandType.Build, true)), + commands.registerCommand(DafnyCommands.Run, () => + buildRunOrTest(installer, CommandType.Run, false)), + commands.registerCommand(DafnyCommands.Test, () => + buildRunOrTest(installer, CommandType.Test, false)) ); return new CompileCommands(); } } -async function buildOrRun(installer: DafnyInstaller, useCustomArgs: boolean, run: boolean): Promise { +// Build: run == false && test == false +// Run: run == true +// Test: run == false && test == true +async function buildRunOrTest(installer: DafnyInstaller, commandType: CommandType, useCustomArgs: boolean): Promise { const document = window.activeTextEditor?.document; if(document == null) { return false; @@ -34,7 +48,7 @@ async function buildOrRun(installer: DafnyInstaller, useCustomArgs: boolean, run if(!await document.save()) { return false; } - const compilerCommand = await new CommandFactory(installer, document.fileName, useCustomArgs, run).createCompilerCommand(); + const compilerCommand = await new CommandFactory(installer, document.fileName, commandType, useCustomArgs).createCompilerCommand(); if(compilerCommand == null) { return false; } @@ -52,8 +66,8 @@ class CommandFactory { public constructor( private readonly installer: DafnyInstaller, private readonly fileName: string, - private readonly useCustomArgs: boolean, - private readonly run: boolean + private readonly commandType: CommandType, + private readonly useCustomArgs: boolean ) {} public async createCompilerCommand(): Promise { @@ -101,14 +115,21 @@ class CommandFactory { } private withCompileAndRun(args: string[]): string[] { - if(this.run) { - return [ 'run', ...args ]; + if(this.commandType === CommandType.Run) { + return [ 'run', '--no-verify', ...args ]; + } + if(this.commandType === CommandType.Test) { + return [ 'test', '--no-verify', ...args ]; + } + if(this.commandType === CommandType.Build) { + return [ 'build', ...args ]; } - return [ 'build', ...args ]; + throw new Error(`Unknown command type: ${this.commandType}`); } private withOutputPath(args: string[]): string[] { - if(this.run) { + //if(this.run || this.test) { + if(this.commandType === CommandType.Run || this.commandType === CommandType.Test) { return args; } if(args.some(arg => arg.includes(OutputPathArg))) {