This patch modifies the grammars of pragmas Abstract_State, Depends, Global, Initializes, Refined_Depends, Refined_Global and Refined_State to explicitly request a single argument. No need for a test as this is a documentation enhancement.
Tested on x86_64-pc-linux-gnu, committed on trunk 2015-11-18 Hristian Kirtchev <kirtc...@adacore.com> * sem_prag.adb (Analyze_Pragma): Update the grammars of pragmas Abstract_State, Depends, Global, Initializes, Refined_Depends, Refined_Global and Refined_State.
Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 230522) +++ sem_prag.adb (working copy) @@ -9998,7 +9998,7 @@ -- ABSTRACT_STATE_LIST ::= -- null -- | STATE_NAME_WITH_OPTIONS - -- | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS} ) + -- | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS}) -- STATE_NAME_WITH_OPTIONS ::= -- STATE_NAME @@ -10018,7 +10018,7 @@ -- EXTERNAL_PROPERTY_LIST ::= -- EXTERNAL_PROPERTY - -- | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY} ) + -- | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY}) -- EXTERNAL_PROPERTY ::= -- Async_Readers [=> boolean_EXPRESSION] @@ -13412,8 +13412,8 @@ -- pragma Depends (DEPENDENCY_RELATION); -- DEPENDENCY_RELATION ::= - -- null - -- | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE} + -- null + -- | (DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}) -- DEPENDENCY_CLAUSE ::= -- OUTPUT_LIST =>[+] INPUT_LIST @@ -14945,9 +14945,9 @@ -- pragma Global (GLOBAL_SPECIFICATION); -- GLOBAL_SPECIFICATION ::= - -- null - -- | GLOBAL_LIST - -- | MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST} + -- null + -- | (GLOBAL_LIST) + -- | (MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}) -- MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST @@ -15689,20 +15689,18 @@ -- Initializes -- ----------------- - -- pragma Initializes (INITIALIZATION_SPEC); + -- pragma Initializes (INITIALIZATION_LIST); - -- INITIALIZATION_SPEC ::= null | INITIALIZATION_LIST - -- INITIALIZATION_LIST ::= - -- INITIALIZATION_ITEM - -- | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM}) + -- null + -- | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM}) -- INITIALIZATION_ITEM ::= name [=> INPUT_LIST] -- INPUT_LIST ::= - -- null - -- | INPUT - -- | (INPUT {, INPUT}) + -- null + -- | INPUT + -- | (INPUT {, INPUT}) -- INPUT ::= name @@ -19287,8 +19285,8 @@ -- pragma Refined_Depends (DEPENDENCY_RELATION); -- DEPENDENCY_RELATION ::= - -- null - -- | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE} + -- null + -- | (DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}) -- DEPENDENCY_CLAUSE ::= -- OUTPUT_LIST =>[+] INPUT_LIST @@ -19363,9 +19361,9 @@ -- pragma Refined_Global (GLOBAL_SPECIFICATION); -- GLOBAL_SPECIFICATION ::= - -- null - -- | GLOBAL_LIST - -- | MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST} + -- null + -- | (GLOBAL_LIST) + -- | (MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}) -- MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST @@ -19488,15 +19486,14 @@ -- pragma Refined_State (REFINEMENT_LIST); -- REFINEMENT_LIST ::= - -- REFINEMENT_CLAUSE - -- | (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE}) + -- (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE}) -- REFINEMENT_CLAUSE ::= state_NAME => CONSTITUENT_LIST -- CONSTITUENT_LIST ::= - -- null - -- | CONSTITUENT - -- | (CONSTITUENT {, CONSTITUENT}) + -- null + -- | CONSTITUENT + -- | (CONSTITUENT {, CONSTITUENT}) -- CONSTITUENT ::= object_NAME | state_NAME