V809-013: Add 'subprogram box' command

The command is based on the LSP DocumentSymbols request to
retrieve the enclosing subprogram, if any.

Author: AnthonyLeonardoGracio

integration/vscode/ada/package.json

@@ -418,6 +418,10 @@
             {
                 "command": "ada.otherFile",
                 "title": "Go to other Ada file"
+            },
+            {
+                "command": "ada.subprogramBox",
+                "title": "Add subprogram box"
             }
         ],
         "keybindings": [
@@ -461,4 +465,4 @@
         "vscode-languageclient": "7.0.0",
         "ws": "8.5.0"
     }
-}
+}

integration/vscode/ada/src/extension.ts

@@ -27,6 +27,7 @@ import * as process from 'process';
 import GPRTaskProvider from './gprTaskProvider';
 import cleanTaskProvider from './cleanTaskProvider';
 import gnatproveTaskProvider from './gnatproveTaskProvider';
+import { getSubprogramSymbol } from './gnatproveTaskProvider';
 import { alsCommandExecutor } from './alsExecuteCommand';
 import { ALSClientFeatures } from './alsClientFeatures';
 import { string } from 'fp-ts';
@@ -41,6 +42,47 @@ let alsTaskProvider: vscode.Disposable[] = [
     ),
 ];
 
+/**
+ * Add a subprogram box above the subprogram enclosing the cursor's position, if any.
+ *
+ * @example:
+ *
+ *  -------
+ *  - Foo -
+ *  -------
+ *
+ *  procedure Foo is
+ */
+function addSupbrogramBox() {
+    const activeEditor = vscode.window.activeTextEditor;
+
+    getSubprogramSymbol(activeEditor)
+        .then(symbol => {
+            if (symbol !== null) {
+                const name: string = symbol.name ?? ""
+                const insertPos = new vscode.Position(symbol.range.start.line, 0);
+                const indentationRange = new vscode.Range(insertPos, symbol.range.start)
+                const indentation: string = activeEditor?.document.getText(indentationRange) ?? ""
+                const eol: string = activeEditor?.document.eol == vscode.EndOfLine.CRLF ? "\r\n" : "\n";
+
+                // Generate the subprogram box after retrieving the indentation of the line of
+                // the subprogram's body declaration.
+                let text: string = indentation + "---" + '-'.repeat(name.length) + "---" + eol
+                    + indentation + "-- " + name + " --" + eol
+                    + indentation + "---" + '-'.repeat(name.length) + "---" + eol
+                    + eol;
+
+                activeEditor?.document.eol.toString
+                if (activeEditor) {
+
+                    activeEditor.edit(editBuilder => {
+                        editBuilder.insert(insertPos, text);
+                    });
+                }
+            }
+        })
+}
+
 export function activate(context: vscode.ExtensionContext): void {
     function createClient(id: string, name: string, extra: string[], pattern: string) {
         let serverModule = context.asAbsolutePath(process.platform + '/ada_language_server');
@@ -125,6 +167,7 @@ export function activate(context: vscode.ExtensionContext): void {
 
     context.subscriptions.push(vscode.workspace.onDidChangeConfiguration(configChanged));
     context.subscriptions.push(vscode.commands.registerCommand('ada.otherFile', otherFileHandler));
+    context.subscriptions.push(vscode.commands.registerCommand('ada.subprogramBox', addSupbrogramBox));
 
     //  Check if we need to add some source directories to the workspace (e.g: when imported projects'
     //  source directories are not placed under the root project's directory).

integration/vscode/ada/src/gnatproveTaskProvider.ts

@@ -15,8 +15,10 @@
 -- of the license.                                                          --
 ----------------------------------------------------------------------------*/
 
+import { none } from 'fp-ts/lib/Option';
 import * as vscode from 'vscode';
 import { SymbolKind } from 'vscode';
+import { integer } from 'vscode-languageclient';
 
 enum taskKinds {
     examineProject,    // Examine the project
@@ -63,13 +65,19 @@ export default class gnatproveTaskProvider implements vscode.TaskProvider<vscode
         else if (definition.taskKind == taskKinds.examineSubprogram
                  || definition.taskKind == taskKinds.proveSubprogram)
         {
-            return getSubprogram(vscode.window.activeTextEditor)
-                .then(subprogram =>
+            return getSubprogramSymbol(vscode.window.activeTextEditor)
+                .then(Symbol =>
                 {
-                    let args = (definition.taskKind == taskKinds.examineSubprogram) ? ['--mode=flow'] : [];
-                    args = getGnatproveArgs(args.concat(['-u', '${fileBasename}', '--limit-subp=${fileBasename}:' + subprogram]));
-                    const shell = new vscode.ShellExecution('gnatprove', args);
-                    return new vscode.Task(definition, vscode.TaskScope.Workspace, task.name, 'ada', shell, '$ada');
+                    if (Symbol) {
+                        const subprogram_line: string = (Symbol.range.start.line + 1).toString()
+                        let args = (definition.taskKind == taskKinds.examineSubprogram) ? ['--mode=flow'] : [];
+                        args = getGnatproveArgs(args.concat(['-u', '${fileBasename}', '--limit-subp=${fileBasename}:' + subprogram_line]));
+                        const shell = new vscode.ShellExecution('gnatprove', args);
+                        return new vscode.Task(definition, vscode.TaskScope.Workspace, task.name, 'ada', shell, '$ada');
+                    }
+                    else {
+                        return task;
+                    }
                 });
         }
         else {
@@ -161,8 +169,16 @@ const getTasks = (): vscode.Task[] => {
     return result;
 };
 
-const getSubprogram = async (editor: vscode.TextEditor | undefined): Promise<string> => {
-    let subprogramLine = 0;
+/**
+ * Return the DocumentSymbol associated to the subprogram enclosing the
+ * the given editor's cursor position, if any.
+ * @param {vscode.TextEditor | undefined} editor - The editor in which we want
+ * to find the suprogram's body enclosing the cursor's position.
+ * @return {vscode.DocumentSymbol | null} Return the symbol corresponding to the
+ * enclosing subprogram or null if not found.
+ */
+export const getSubprogramSymbol = async (editor: vscode.TextEditor | undefined): Promise<vscode.DocumentSymbol|null> => {
+      let subprogramLine = 0;
     if (editor) {
         const line = editor.selection.active.line;
 
@@ -190,12 +206,12 @@ const getSubprogram = async (editor: vscode.TextEditor | undefined): Promise<str
         let scopeSymbols = subprograms.filter(sym => line >= sym.range.start.line && line <= sym.range.end.line);
         if (scopeSymbols.length > 0) {
             scopeSymbols.sort((a,b) => (a.range.end.line - a.range.start.line) - (b.range.end.line - b.range.start.line));
-            subprogramLine = scopeSymbols[0].range.start.line;
+            return scopeSymbols[0];
         };
     };
-    // Line numbers start at 0 in VS Code, and at 1 in GNAT
-    return (subprogramLine + 1).toString();
-};
+
+    return null;
+}
 
 const getSelectedRegion = (editor: vscode.TextEditor | undefined): string => {
     if (editor) {