[Ada] Display source code pointing at locations in messages for GNATprove

gcc/ada/

	* errout.adb: (Error_Msg-Internal): Pass the location for a line
	insertion if any in the message.
	(Output_Messages: Add display of source code lines if -gnatdF is
	set.
	(Write_Source_Code_Line): Code clean up.
	* erroutc.adb (Prescan_Message): Apply prescan for continuation
	lines when -gnatdF is set, and record presence of line
	insertion.
	* erroutc.ads (Has_Insertion_Line): New global for prescan.
	(Error_Msg_Object): Add field to record line insertion if
	present.
	* errutil.adb (Error_Msg): Pass no location for Insertion_Sloc.

1 files changed, 9 insertions, 2 deletions

diff --git a/gcc/ada/erroutc.adb b/gcc/ada/erroutc.adb
index df174f6..93f53bb 100644
--- a/gcc/ada/erroutc.adb
+++ b/gcc/ada/erroutc.adb
@@ -814,9 +814,9 @@ package body Erroutc is
       J : Natural;
 
    begin
-      --  Nothing to do for continuation line
+      --  Nothing to do for continuation line, unless -gnatdF is set
 
-      if Msg (Msg'First) = '\' then
+      if not Debug_Flag_FF and then Msg (Msg'First) = '\' then
          return;
       end if;
 
@@ -826,6 +826,7 @@ package body Erroutc is
       Is_Unconditional_Msg := False;
       Is_Warning_Msg       := False;
       Has_Double_Exclam    := False;
+      Has_Insertion_Line   := False;
 
       --  Check style message
 
@@ -903,6 +904,12 @@ package body Erroutc is
                J := J + 1;
             end if;
 
+         --  Insertion line (# insertion)
+
+         elsif Msg (J) = '#' then
+            Has_Insertion_Line := True;
+            J := J + 1;
+
          --  Non-serious error (| insertion)
 
          elsif Msg (J) = '|' then