2011-08-01 Yannick Moy <moy@adacore.com>

	* err_vars.ads (Error_Msg_Lang, Error_Msg_Langlen): new variables for
	insertion character ~~
	* errout.ads, errout.adb (Formal_Error_Msg_...): remove procedures
	(Set_Error_Msg_Lang): new procedure which fixes the language for use
	with insertion character ~~
	(Set_Msg_Text): treat insertion character ~~
	* par-ch4.adb, par-ch5.adb, par-endh.adb, sem_attr.adb, sem_ch11.adb,
	sem_ch3.adb, sem_ch5.adb, sem_ch9.adb, sem_util.adb: Replace calls to
	Formal_Error_Msg_... procedures by equivalent Error_Msg_...
	procedures. Favor calls to Error_Msg_F(E) over Error_Msg_N(E). Make
	errors related to the formal language restriction not serious
	(insertion character |).
	* par.adb (Par): set formal language for error messages if needed
	* sem_ch6.adb (Check_Missing_Return): take into account possible
	generated statements at the end of the function
	* snames.ads-tmpl (Name_SPARK_95, Pragma_SPARK_95): new variable and
	enumeration value to define a new pragma SPARK_95
	* opt.ads, opt.adb (SPARK_Version_Type, SPARK_Version_Default,
	SPARK_Version): new type and variables to store the SPARK version
	(none by default).
	(SPARK_Mode): return True when SPARK_Version is set
	* par-prag.adb: Correct indentation
	(Prag): take Pragma_SPARK_95 into account
	* sem_prag.adb (Set_Mechanism_Value, Sig_Flags): take Pragma_SPARK_95
	into account.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177056 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 34 insertions, 22 deletions

diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index 8ddd2209ad6..502cb70b253 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -439,37 +439,37 @@ begin
          List_Pragmas.Increment_Last;
          List_Pragmas.Table (List_Pragmas.Last) := (Page, Semi);
 
-         ------------------
-         -- Restrictions --
-         ------------------
+      ------------------
+      -- Restrictions --
+      ------------------
 
-         --  pragma Restrictions (RESTRICTION {, RESTRICTION});
+      --  pragma Restrictions (RESTRICTION {, RESTRICTION});
 
-         --  RESTRICTION ::=
-         --    restriction_IDENTIFIER
-         --  | restriction_parameter_IDENTIFIER => EXPRESSION
+      --  RESTRICTION ::=
+      --    restriction_IDENTIFIER
+      --  | restriction_parameter_IDENTIFIER => EXPRESSION
 
-         --  We process the case of No_Obsolescent_Features, since this has
-         --  a syntactic effect that we need to detect at parse time (the use
-         --  of replacement characters such as colon for pound sign).
+      --  We process the case of No_Obsolescent_Features, since this has
+      --  a syntactic effect that we need to detect at parse time (the use
+      --  of replacement characters such as colon for pound sign).
 
-         when Pragma_Restrictions =>
-            Process_Restrictions_Or_Restriction_Warnings;
+      when Pragma_Restrictions =>
+         Process_Restrictions_Or_Restriction_Warnings;
 
-         --------------------------
-         -- Restriction_Warnings --
-         --------------------------
+      --------------------------
+      -- Restriction_Warnings --
+      --------------------------
 
-         --  pragma Restriction_Warnings (RESTRICTION {, RESTRICTION});
+      --  pragma Restriction_Warnings (RESTRICTION {, RESTRICTION});
 
-         --  RESTRICTION ::=
-         --    restriction_IDENTIFIER
-         --  | restriction_parameter_IDENTIFIER => EXPRESSION
+      --  RESTRICTION ::=
+      --    restriction_IDENTIFIER
+      --  | restriction_parameter_IDENTIFIER => EXPRESSION
 
-         --  See above comment for pragma Restrictions
+      --  See above comment for pragma Restrictions
 
-         when Pragma_Restriction_Warnings =>
-            Process_Restrictions_Or_Restriction_Warnings;
+      when Pragma_Restriction_Warnings =>
+         Process_Restrictions_Or_Restriction_Warnings;
 
       ----------------------------------------------------------
       -- Source_File_Name and Source_File_Name_Project (GNAT) --
@@ -889,6 +889,18 @@ begin
          end if;
       end Source_Reference;
 
+      --------------
+      -- SPARK_95 --
+      --------------
+
+      --  This pragma must be processed at parse time, since we want to set
+      --  the SPARK version properly at parse time to recognize the appropriate
+      --  SPARK version syntax.
+
+      when Pragma_SPARK_95 =>
+         SPARK_Version := SPARK_95;
+         Set_Error_Msg_Lang ("(" & Formal_Language & ") ");
+
       -------------------------
       -- Style_Checks (GNAT) --
       -------------------------