Merge remote branch 'origin/master' into edge

Author: automatic-merge

README.md

@@ -58,6 +58,7 @@ extension at
       - [Ada: Go to other file](#ada-go-to-other-file)
       - [Ada: Add subprogram box](#ada-add-subprogram-box)
       - [Ada: Reload project](#ada-reload-project)
+      - [Tasks with keyboard shortcuts](#tasks-with-keyboard-shortcuts)
     - [Bug Reporting](#bug-reporting)
     - [Limitations and Differences with GNAT Studio](#limitations-and-differences-with-gnat-studio)
   - [Integration with other editors and IDEs](#integration-with-other-editors-and-ides)
@@ -331,6 +332,30 @@ The default shortcut is `Alt+Shift+B`.
 This command reloads the current project.
 The default shortcut is `None`.
 
+#### Tasks with keyboard shortcuts
+
+The following default shortcuts are provided for tasks:
+
+| Task                           | Shortcut        |
+|--------------------------------|-----------------|
+| `spark: Prove file`            | `Meta+Y Meta+F` |
+| `spark: Prove subprogram`      | `Meta+Y Meta+S` |
+| `spark: Prove selected region` | `Meta+Y Meta+R` |
+| `spark: Prove line`            | `Meta+Y Meta+L` |
+
+`Meta` = ⌘ on macOS, `Win` on Windows, `Meta` on Linux
+
+These shortcuts can be customized and new shortcuts can be added for other tasks by using the command `Preferences: Open Keyboard Shortcuts (JSON)` and adding entries like the following example:
+
+```json
+{
+    "command": "workbench.action.tasks.runTask",
+    "args": "ada: Check current file",
+    "key": "meta+y meta+c",
+    "when": "editorLangId == ada && editorTextFocus"
+}
+```
+
 ### Bug Reporting
 
 You can use the VS Code `Issue Reporter` to report issues. Just click on the `Help -> Report Issue` menu, select `An extension` for the `File on` entry and `Language Support for Ada` for the extension name. Put as many information you can in the description, like steps to reproduce, stacktraces or system information (VS Code automatically includes it by default). This will create a GitHub issue in the [Ada Language Server](https://github.com/AdaCore/ada_language_server/) repository.

integration/vscode/ada/package.json

@@ -787,6 +787,30 @@
                 "command": "ada.subprogramBox",
                 "key": "alt+shift+B",
                 "when": "editorLangId == ada && editorTextFocus"
+            },
+            {
+                "command": "workbench.action.tasks.runTask",
+                "args": "spark: Prove file",
+                "key": "meta+y meta+f",
+                "when": "editorLangId == ada && editorTextFocus"
+            },
+            {
+                "command": "workbench.action.tasks.runTask",
+                "args": "spark: Prove subprogram",
+                "key": "meta+y meta+s",
+                "when": "editorLangId == ada && editorTextFocus"
+            },
+            {
+                "command": "workbench.action.tasks.runTask",
+                "args": "spark: Prove selected region",
+                "key": "meta+y meta+r",
+                "when": "editorLangId == ada && editorTextFocus"
+            },
+            {
+                "command": "workbench.action.tasks.runTask",
+                "args": "spark: Prove line",
+                "key": "meta+y meta+l",
+                "when": "editorLangId == ada && editorTextFocus"
             }
         ],
         "menus": {

integration/vscode/ada/src/commands.ts

@@ -684,11 +684,9 @@ function getLimitSubpArg(filename: string, range: vscode.Range) {
  * to the current editor's selection.
  */
 export const sparkLimitRegionArg = (): Promise<string[]> => {
-    return new Promise((resolve) => {
-        resolve([
-            `--limit-region=\${fileBasename}:${getSelectedRegion(vscode.window.activeTextEditor)}`,
-        ]);
-    });
+    return Promise.resolve([
+        `--limit-region=\${fileBasename}:${getSelectedRegion(vscode.window.activeTextEditor)}`,
+    ]);
 };
 
 /**
@@ -711,6 +709,10 @@ export const getSelectedRegion = (editor: vscode.TextEditor | undefined): string
 /**
  * Return the closest DocumentSymbol of the given kinds enclosing the
  * the given editor's cursor position, if any.
+ *
+ * If the given editor is undefined or not on an Ada file, the function returns
+ * `null` immediately.
+ *
  * @param editor - The editor in which we want
  * to find the closest symbol enclosing the cursor's position.
  * @returns Return the closest enclosing symbol.
@@ -720,7 +722,7 @@ export async function getEnclosingSymbol(
     editor: vscode.TextEditor | undefined,
     kinds: vscode.SymbolKind[]
 ): Promise<vscode.DocumentSymbol | null> {
-    if (editor) {
+    if (editor && editor.document.languageId == 'ada') {
         const line = editor.selection.active.line;
 
         // First get all symbols for current file
@@ -758,6 +760,12 @@ export async function getEnclosingSymbol(
  *
  * It is implemented by fetching the 'Prove subbprogram' task and using it as a
  * template such that the User can customize the task to impact the CodeLens.
+ *
+ * Another option could have been to use the command
+ * `workbench.action.tasks.runTask` with the name of the SPARK task as argument
+ * however that would run the task using the current cursor location which may
+ * not match the CodeLens that was triggered. So it is better to create a task
+ * dedicated to the location of the CodeLens.
  */
 async function sparkProveSubprogram(
     uri: vscode.Uri,

integration/vscode/ada/src/extension.ts

@@ -31,6 +31,14 @@ import {
     getEvaluatedTerminalEnv,
     startedInDebugMode,
 } from './helpers';
+/**
+ * This import gives access to the package.json content.
+ */
+import * as meta from '../package.json';
+
+// eslint-disable-next-line max-len
+// eslint-disable-next-line @typescript-eslint/no-unsafe-assignment, @typescript-eslint/no-unsafe-member-access
+export const EXTENSION_NAME: string = meta.displayName;
 
 const ADA_CONTEXT = 'ADA_PROJECT_CONTEXT';
 

integration/vscode/ada/src/helpers.ts

@@ -22,9 +22,9 @@ import { CancellationError, CancellationToken, DocumentSymbol, SymbolKind } from
 import { LanguageClient } from 'vscode-languageclient/node';
 import winston from 'winston';
 // eslint-disable-next-line @typescript-eslint/no-unused-vars
-import { ExtensionState } from './ExtensionState';
-import { adaExtState, logger } from './extension';
 import { existsSync } from 'fs';
+import { ExtensionState } from './ExtensionState';
+import { EXTENSION_NAME, adaExtState, logger, mainOutputChannel } from './extension';
 
 /**
  * Substitue any variable reference present in the given string. VS Code
@@ -480,3 +480,22 @@ export function which(execName: string) {
 
     return exePath;
 }
+
+/**
+ * Show an error message with a button "Open Log" that opens the main extension
+ * log (not the Ada LS or the GPR LS)
+ *
+ * @param msg - the message to display
+ * @param options - message options to pass to {@link vscode.window.showErrorMessage}
+ */
+export async function showErrorMessageWithOpenLogButton(
+    msg: string,
+    options?: vscode.MessageOptions
+) {
+    const answer = await vscode.window.showErrorMessage<vscode.MessageItem>(msg, options ?? {}, {
+        title: `Open ${EXTENSION_NAME} Extension Log`,
+    });
+    if (answer) {
+        mainOutputChannel.show();
+    }
+}

integration/vscode/ada/src/taskProviders.ts

@@ -19,8 +19,8 @@ import assert from 'assert';
 import { basename } from 'path';
 import * as vscode from 'vscode';
 import { CMD_GPR_PROJECT_ARGS } from './commands';
-import { adaExtState } from './extension';
-import { AdaMain, getAdaMains } from './helpers';
+import { adaExtState, logger } from './extension';
+import { AdaMain, getAdaMains, showErrorMessageWithOpenLogButton } from './helpers';
 
 export const TASK_TYPE_ADA = 'ada';
 export const TASK_TYPE_SPARK = 'spark';
@@ -462,9 +462,12 @@ export class SimpleTaskProvider implements vscode.TaskProvider {
              * resolved tasks, hence we must resolve pre-defined tasks here.
              */
             const resolvedTask = await this.resolveTask(task, token);
-            assert(resolvedTask);
 
-            result.push(resolvedTask);
+            if (resolvedTask) {
+                result.push(resolvedTask);
+            } else {
+                logger.error(`Failed to resolve task: ${JSON.stringify(task, undefined, 2)}`);
+            }
         }
 
         return result;
@@ -520,10 +523,12 @@ export class SimpleTaskProvider implements vscode.TaskProvider {
                 execution = new vscode.ShellExecution(taskDef.command, evaluatedArgs);
             } catch (err) {
                 let msg = 'Error while evaluating task arguments.';
+                logger.error(msg);
+                logger.error(err);
                 if (err instanceof Error) {
                     msg += ' ' + err.message;
                 }
-                void vscode.window.showErrorMessage(msg);
+                void showErrorMessageWithOpenLogButton(msg);
                 return undefined;
             }
         }

integration/vscode/ada/tsconfig.json

@@ -15,7 +15,8 @@
         "forceConsistentCasingInFileNames": true,
         "noImplicitReturns": true,
         "noFallthroughCasesInSwitch": true,
-        "noUnusedParameters": true
+        "noUnusedParameters": true,
+        "resolveJsonModule": true
     },
     "exclude": ["node_modules", "out"],
     "include": ["test", "src"]