[Enhancement]: Make the Ada Language Server automatically SPARK‑aware

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.

No files, tests, or implementation entry points are identified. Start by locating how the language server reads SPARK_Mode and how completion, diagnostics, signature help, hovers, definitions, refactorings, and code actions obtain Ada semantics. Done means SPARK-aware behavior is applied at the requested granularity while non-SPARK units retain full Ada behavior.