Add a new character sequence [] for error codes in error messages
handled by Error_Msg procedures, to use for SPARK-related errors.
Display of additional information on the error or warning based on
the error code is delegated to GNATprove.

gcc/ada/

	* err_vars.ads (Error_Msg_Code): New variable for error codes.
	* errout.adb (Error_Msg_Internal): Display continuation message
	when an error code was present.
	(Set_Msg_Text): Handle character sequence [] for error codes.
	* errout.ads: Document new insertion sequence [].
	(Error_Msg_Code): New renaming.
	* erroutc.adb (Prescan_Message): Detect presence of error code.
	(Set_Msg_Insertion_Code): Handle new insertion sequence [].
	* erroutc.ads (Has_Error_Code): New variable for prescan.
	(Set_Msg_Insertion_Code): Handle new insertion sequence [].
	* contracts.adb (Check_Type_Or_Object_External_Properties):
	Replace reference to SPARK RM section by an error code.
	* sem_elab.adb (SPARK_Processor): Same.
	* sem_prag.adb (Check_Missing_Part_Of): Same.
	* sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Same.