Enhancement Request
Explanation
When source code is in SPARK_Mode => On (via aspect, pragma, or project configuration), ALS should restrict all LSP features (completion, diagnostics, signature help, etc.) to the SPARK subset of Ada. The goal is to prevent non‑SPARK constructs from being suggested or silently accepted and to make SPARK development smoother and more accurate.
Expected behavior
In SPARK mode, completions should exclude disallowed features (e.g., tasking, unrestricted general access types, etc.) and actively propose SPARK contracts and idioms (Pre, Post, Global, Depends, use of 'Old, etc.). Diagnostics should flag use of non‑SPARK constructs immediately; hovers/definition lookups should prioritize or clearly mark SPARK‑valid entities; and refactorings/code actions should preserve SPARK compliance. Non‑SPARK units continue to receive full Ada behavior.
Activation & Scope
Behavior should be automatic based on SPARK_Mode, with granularity matching where it applies (per unit/spec/body or subprogram) and respecting project‑wide configuration pragmas. A manual override setting (e.g., auto/on/off) is acceptable but optional. This request targets LSP‑level semantics only (not GNATprove integration), though SPARK‑oriented completion and diagnostics are in scope.
Enhancement Request
Explanation
When source code is in SPARK_Mode => On (via aspect, pragma, or project configuration), ALS should restrict all LSP features (completion, diagnostics, signature help, etc.) to the SPARK subset of Ada. The goal is to prevent non‑SPARK constructs from being suggested or silently accepted and to make SPARK development smoother and more accurate.
Expected behavior
In SPARK mode, completions should exclude disallowed features (e.g., tasking, unrestricted general access types, etc.) and actively propose SPARK contracts and idioms (Pre, Post, Global, Depends, use of 'Old, etc.). Diagnostics should flag use of non‑SPARK constructs immediately; hovers/definition lookups should prioritize or clearly mark SPARK‑valid entities; and refactorings/code actions should preserve SPARK compliance. Non‑SPARK units continue to receive full Ada behavior.
Activation & Scope
Behavior should be automatic based on SPARK_Mode, with granularity matching where it applies (per unit/spec/body or subprogram) and respecting project‑wide configuration pragmas. A manual override setting (e.g., auto/on/off) is acceptable but optional. This request targets LSP‑level semantics only (not GNATprove integration), though SPARK‑oriented completion and diagnostics are in scope.