Skip to content

Commit a55dccf

Browse files
author
mergerepo
committed
Merge remote branch 'origin/master' into edge
(no-precommit-check no-tn-check)
2 parents c0b38a0 + 39b4b9f commit a55dccf

File tree

14 files changed

+1096
-53
lines changed

14 files changed

+1096
-53
lines changed

‎README.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,8 @@ The extension includes a task provider. It provides two "auto-detected" tasks
169169
(under `/Terminal/Run Task...` menu):
170170
* "ada: Build current project" - launch `gprbuild` to build the current GPR project
171171
* "ada: Check current file" - launch `gprbuild` to check errors in the current editor
172+
* "ada: Run gnatprove on the current project" - launch `gnatprove` for the current GPR project
173+
* "ada: Run gnatprove on the current file" - launch `gnatprove` to check errors in the current editor
172174

173175
You can bind keyboard shortcuts to them by adding to the `keybindings.json` file:
174176

‎integration/vscode/ada/package.json

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@
183183
],
184184
"pattern": [
185185
{
186-
"regexp": "^([^:]:?[^:]*):(\\d+):(\\d+):\\s+(warning|)(?:[:]\\s+)?(.*)$",
186+
"regexp": "^([^:]:?[^:]*):(\\d+):(\\d+):\\s+(?:([a-z]+):\\s+)?(.*)$",
187187
"file": 1,
188188
"line": 2,
189189
"column": 3,
@@ -209,6 +209,22 @@
209209
"description": "Just check the current file only"
210210
}
211211
}
212+
},
213+
{
214+
"type": "gnatprove",
215+
"required": [
216+
"projectFile"
217+
],
218+
"properties": {
219+
"projectFile": {
220+
"type": "string",
221+
"description": "The project file"
222+
},
223+
"taskKind": {
224+
"type": "integer",
225+
"description": "Check the current file only or whole project"
226+
}
227+
}
212228
}
213229
],
214230
"commands": [
@@ -256,4 +272,4 @@
256272
"vscode-languageclient": "^7.0.0",
257273
"ws": "^7.5.2"
258274
}
259-
}
275+
}

‎integration/vscode/ada/src/extension.ts

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,16 @@ import * as vscode_languageclient from 'vscode-languageclient/node';
2020
import * as process from 'process';
2121

2222
import GPRTaskProvider from './gprTaskProvider';
23+
import gnatproveTaskProvider from './gnatproveTaskProvider';
2324

24-
let alsTaskProvider: undefined | vscode.Disposable = vscode.tasks.registerTaskProvider(
25-
GPRTaskProvider.gprBuildType,
26-
new GPRTaskProvider()
27-
);
25+
let alsTaskProvider: vscode.Disposable[] = [
26+
vscode.tasks.registerTaskProvider(GPRTaskProvider.gprBuildType, new GPRTaskProvider()),
27+
28+
vscode.tasks.registerTaskProvider(
29+
gnatproveTaskProvider.gnatproveType,
30+
new gnatproveTaskProvider()
31+
),
32+
];
2833

2934
export function activate(context: vscode.ExtensionContext): void {
3035
let serverModule = context.asAbsolutePath(process.platform + '/ada_language_server');
@@ -81,8 +86,8 @@ export function activate(context: vscode.ExtensionContext): void {
8186
}
8287

8388
export function deactivate(): void {
84-
if (alsTaskProvider) {
85-
alsTaskProvider.dispose();
86-
alsTaskProvider = undefined;
89+
for (const item of alsTaskProvider) {
90+
item.dispose();
8791
}
92+
alsTaskProvider = [];
8893
}

‎integration/vscode/ada/src/gnatproveTaskProvider.ts

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
/*----------------------------------------------------------------------------
2+
-- Language Server Protocol --
3+
-- --
4+
-- Copyright (C) 2018-2021, AdaCore --
5+
-- --
6+
-- This is free software; you can redistribute it and/or modify it under --
7+
-- terms of the GNU General Public License as published by the Free Soft- --
8+
-- ware Foundation; either version 3, or (at your option) any later ver- --
9+
-- sion. This software is distributed in the hope that it will be useful, --
10+
-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN- --
11+
-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public --
12+
-- License for more details. You should have received a copy of the GNU --
13+
-- General Public License distributed with this software; see file --
14+
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy --
15+
-- of the license. --
16+
----------------------------------------------------------------------------*/
17+
18+
import * as vscode from 'vscode';
19+
20+
enum taskKinds {
21+
proveProject, // Run gnatprove for the project
22+
proveFile, // Run gnatprove for the single file
23+
}
24+
25+
export default class gnatproveTaskProvider implements vscode.TaskProvider<vscode.Task> {
26+
public static gnatproveType = 'gnatprove';
27+
gnatproveTasks: vscode.Task[] | undefined;
28+
29+
constructor() {
30+
this.gnatproveTasks = undefined;
31+
}
32+
33+
// eslint-disable-next-line @typescript-eslint/no-unused-vars
34+
provideTasks(_token: vscode.CancellationToken): vscode.Task[] {
35+
if (!this.gnatproveTasks) {
36+
this.gnatproveTasks = getTasks();
37+
}
38+
return this.gnatproveTasks;
39+
}
40+
41+
resolveTask(
42+
task: vscode.Task,
43+
// eslint-disable-next-line @typescript-eslint/no-unused-vars
44+
_token: vscode.CancellationToken
45+
): vscode.ProviderResult<vscode.Task> {
46+
return task;
47+
}
48+
}
49+
50+
const getTasks = (): vscode.Task[] => {
51+
function makeTask(taskKind: taskKinds, args: string[], title: string) {
52+
const kind = {
53+
type: gnatproveTaskProvider.gnatproveType,
54+
projectFile: '${config:ada.projectFile}',
55+
taskKind: taskKind,
56+
};
57+
const shell = new vscode.ShellExecution('gnatprove', args);
58+
const task = new vscode.Task(kind, vscode.TaskScope.Workspace, title, 'ada', shell, '$ada');
59+
task.group = vscode.TaskGroup.Build;
60+
return task;
61+
}
62+
63+
const result: vscode.Task[] = [];
64+
65+
// Run gnatprove on current project
66+
const proveProject = makeTask(
67+
taskKinds.proveProject,
68+
getGnatproveArgs('${config:ada.projectFile}'),
69+
'Run gnatprove on the current project'
70+
);
71+
72+
// Run gnatprove on a file
73+
const proveFile = makeTask(
74+
taskKinds.proveFile,
75+
getGnatproveArgs('${config:ada.projectFile}', '${fileBasename}'),
76+
'Run gnatprove on the current file'
77+
);
78+
result.push(proveProject);
79+
result.push(proveFile);
80+
81+
return result;
82+
};
83+
84+
const getGnatproveArgs = (projectFile?: string, file?: string): string[] => {
85+
// Append file (if any) and `-gnatef` to generate full file names in errors/warnings
86+
const arg = file ? [file] : [];
87+
const p_gnatef = ['-cargs', '-gnatef'];
88+
return commonArgs(projectFile).concat(arg, p_gnatef);
89+
};
90+
91+
// return '-P project.gpr -XVAR=value` optiona
92+
const commonArgs = (projectFile?: string): string[] => {
93+
const vars: string[][] = Object.entries(
94+
vscode.workspace.getConfiguration('ada').get('scenarioVariables') ?? []
95+
);
96+
const fold = (args: string[], item: string[]): string[] => {
97+
const option = '-X' + item[0] + '=' + item[1];
98+
return args.concat([option]);
99+
};
100+
// Set projectFile is any
101+
const prj = projectFile ? ['-P', projectFile] : [];
102+
// for each scenarioVariables put `-Xname=value` option
103+
return vars.reduce(fold, prj);
104+
};

‎source/ada/lsp-ada_completions-parameters.adb

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
------------------------------------------------------------------------------
2+
-- Language Server Protocol --
3+
-- --
4+
-- Copyright (C) 2021, AdaCore --
5+
-- --
6+
-- This is free software; you can redistribute it and/or modify it under --
7+
-- terms of the GNU General Public License as published by the Free Soft- --
8+
-- ware Foundation; either version 3, or (at your option) any later ver- --
9+
-- sion. This software is distributed in the hope that it will be useful, --
10+
-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN- --
11+
-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public --
12+
-- License for more details. You should have received a copy of the GNU --
13+
-- General Public License distributed with this software; see file --
14+
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy --
15+
-- of the license. --
16+
------------------------------------------------------------------------------
17+
18+
with Ada.Strings.UTF_Encoding;
19+
20+
with GNATCOLL.Utils;
21+
22+
with Langkit_Support.Text; use Langkit_Support.Text;
23+
with Laltools.Common;
24+
with Libadalang.Common;
25+
26+
with LSP.Ada_Completions.Filters;
27+
with LSP.Lal_Utils;
28+
with LSP.Types; use LSP.Types;
29+
30+
package body LSP.Ada_Completions.Parameters is
31+
32+
------------------------
33+
-- Propose_Completion --
34+
------------------------
35+
36+
overriding procedure Propose_Completion
37+
(Self : Parameter_Completion_Provider;
38+
Sloc : Langkit_Support.Slocs.Source_Location;
39+
Token : Libadalang.Common.Token_Reference;
40+
Node : Libadalang.Analysis.Ada_Node;
41+
Filter : in out LSP.Ada_Completions.Filters.Filter;
42+
Names : out Ada_Completions.Completion_Maps.Map;
43+
Result : out LSP.Messages.CompletionList)
44+
is
45+
pragma Unreferenced (Filter, Names);
46+
use Libadalang.Analysis;
47+
use Libadalang.Common;
48+
49+
Call_Expr_Node : constant Libadalang.Analysis.Call_Expr :=
50+
LSP.Lal_Utils.Get_Call_Expr (Node);
51+
Token_Kind : Libadalang.Common.Token_Kind :=
52+
Kind (Data (Token));
53+
Designators : Laltools.Common.Node_Vectors.Vector;
54+
55+
function Is_Present (Id_Text : Text_Type) return Boolean;
56+
-- Return True if Id_Name match one of the designators
57+
58+
----------------
59+
-- Is_Present --
60+
----------------
61+
62+
function Is_Present (Id_Text : Text_Type) return Boolean is
63+
begin
64+
for Desig of Designators loop
65+
if Id_Text = Desig.Text then
66+
return True;
67+
end if;
68+
end loop;
69+
return False;
70+
end Is_Present;
71+
72+
begin
73+
if Call_Expr_Node = No_Ada_Node then
74+
return;
75+
end if;
76+
77+
Designators := LSP.Lal_Utils.Get_Call_Designators (Call_Expr_Node);
78+
79+
if Token_Kind = Ada_Whitespace then
80+
Token_Kind := Kind (Data (Previous (Token, Exclude_Trivia => True)));
81+
end if;
82+
83+
declare
84+
Item : LSP.Messages.CompletionItem;
85+
Prefix : constant Ada.Strings.UTF_Encoding.UTF_8_String :=
86+
Langkit_Support.Text.To_UTF8 (Node.Text);
87+
Name_Node : constant Libadalang.Analysis.Name :=
88+
Call_Expr_Node.F_Name;
89+
begin
90+
for N of Self.Context.Find_All_Env_Elements (Name_Node) loop
91+
if N.Kind in Ada_Basic_Subp_Decl then
92+
declare
93+
Params_Snippet : LSP_String := Empty_LSP_String;
94+
Snippet_Name : LSP_String := Empty_LSP_String;
95+
-- $0 is used for the final tab stop
96+
Index : Positive := 1;
97+
Spec : constant Libadalang.Analysis.Base_Subp_Spec
98+
:= N.As_Basic_Decl.P_Subp_Spec_Or_Null;
99+
begin
100+
if Spec /= Libadalang.Analysis.No_Base_Subp_Spec
101+
and then LSP.Lal_Utils.Match_Designators
102+
(Spec.P_Params, Designators)
103+
then
104+
for Param of Spec.P_Params loop
105+
for Id of Param.F_Ids loop
106+
declare
107+
Name_Text : constant Text_Type := Id.Text;
108+
Name : constant LSP_String :=
109+
To_LSP_String (Name_Text);
110+
begin
111+
if not Is_Present (Name_Text) then
112+
if Token_Kind in Ada_Par_Open | Ada_Comma
113+
or else
114+
LSP.Types.Starts_With
115+
(Text => Name,
116+
Prefix => Prefix,
117+
Case_Sensitive => False)
118+
then
119+
Item.label := To_Virtual_String (Name);
120+
Item.insertTextFormat :=
121+
(True, LSP.Messages.PlainText);
122+
Item.insertText := (True, Name & " => ");
123+
Item.kind := (True, LSP.Messages.Text);
124+
Result.items.Append (Item);
125+
end if;
126+
127+
Params_Snippet := Params_Snippet
128+
& Name
129+
& " => "
130+
& "$"
131+
& To_LSP_String
132+
(GNATCOLL.Utils.Image
133+
(Index, Min_Width => 1))
134+
& ", ";
135+
Index := Index + 1;
136+
end if;
137+
end;
138+
end loop;
139+
end loop;
140+
141+
-- If the string is empty => nothing to do
142+
if Params_Snippet /= Empty_LSP_String then
143+
-- Remove the last 2 characters which are ", " and
144+
-- replace it by ")" and the final tab stop
145+
Params_Snippet := Unbounded_Slice
146+
(Params_Snippet,
147+
1,
148+
Length (Params_Snippet) - 2);
149+
Params_Snippet := Params_Snippet & ")$0";
150+
151+
Snippet_Name :=
152+
Snippet_Name
153+
& "Params of "
154+
& To_LSP_String (Name_Node.Text);
155+
Item.label := To_Virtual_String
156+
(Snippet_Name);
157+
Item.insertTextFormat :=
158+
(True, LSP.Messages.Snippet);
159+
Item.insertText := (True, Params_Snippet);
160+
Item.kind := (True, LSP.Messages.Snippet);
161+
Result.items.Append (Item);
162+
end if;
163+
end if;
164+
end;
165+
end if;
166+
end loop;
167+
end;
168+
end Propose_Completion;
169+
170+
end LSP.Ada_Completions.Parameters;

‎source/ada/lsp-ada_completions-parameters.ads

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
------------------------------------------------------------------------------
2+
-- Language Server Protocol --
3+
-- --
4+
-- Copyright (C) 2021, AdaCore --
5+
-- --
6+
-- This is free software; you can redistribute it and/or modify it under --
7+
-- terms of the GNU General Public License as published by the Free Soft- --
8+
-- ware Foundation; either version 3, or (at your option) any later ver- --
9+
-- sion. This software is distributed in the hope that it will be useful, --
10+
-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN- --
11+
-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public --
12+
-- License for more details. You should have received a copy of the GNU --
13+
-- General Public License distributed with this software; see file --
14+
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy --
15+
-- of the license. --
16+
------------------------------------------------------------------------------
17+
-- A completion provider for parameters inside a call
18+
19+
with LSP.Ada_Handlers;
20+
21+
package LSP.Ada_Completions.Parameters is
22+
23+
type Parameter_Completion_Provider
24+
(Context : not null LSP.Ada_Handlers.Context_Access)
25+
is new Completion_Provider with null record;
26+
27+
overriding procedure Propose_Completion
28+
(Self : Parameter_Completion_Provider;
29+
Sloc : Langkit_Support.Slocs.Source_Location;
30+
Token : Libadalang.Common.Token_Reference;
31+
Node : Libadalang.Analysis.Ada_Node;
32+
Filter : in out LSP.Ada_Completions.Filters.Filter;
33+
Names : out Ada_Completions.Completion_Maps.Map;
34+
Result : out LSP.Messages.CompletionList);
35+
-- Get completion for keywords, filtering them with the prefix.
36+
37+
end LSP.Ada_Completions.Parameters;

0 commit comments

Comments
 (0)