1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
separate (ErrorHandler)
procedure PrintLine
(Listing : in SPARK_IO.File_Type;
Start_Pos, End_Pos, Indent : in Natural;
Line : in E_Strings.T;
Add_New_Line : in Boolean;
New_Start : out Natural)
is
Pos, Current_Line_End, Current_Line_Start : Natural;
procedure Print_Current_Line
--# global in Add_New_Line;
--# in Current_Line_End;
--# in Current_Line_Start;
--# in Line;
--# in Listing;
--# in out SPARK_IO.File_Sys;
--# derives SPARK_IO.File_Sys from *,
--# Add_New_Line,
--# Current_Line_End,
--# Current_Line_Start,
--# Line,
--# Listing;
is
begin
for Ix in Natural range Current_Line_Start .. Current_Line_End loop
Put_Char (Listing, E_Strings.Get_Element (E_Str => Line,
Pos => Ix));
end loop;
if Current_Line_End /= E_Strings.Get_Length (E_Str => Line) or Add_New_Line then
New_Line (File => Listing,
Spacing => 1);
end if;
end Print_Current_Line;
procedure Find_Current_Line_End (Current_Line_Pos : in Natural)
--# global in Current_Line_Start;
--# in End_Pos;
--# in Line;
--# in Pos;
--# out Current_Line_End;
--# derives Current_Line_End from Current_Line_Pos,
--# Current_Line_Start,
--# End_Pos,
--# Line,
--# Pos;
is
Next_Space_Pos, Current_Space_Pos : Integer;
function Find_Next_Space (Curr_Pos : in Natural) return Natural
--# global in Line;
is
Next_Pos : Natural;
begin
Next_Pos := Curr_Pos;
loop
exit when Next_Pos = E_Strings.Get_Length (E_Str => Line);
Next_Pos := Next_Pos + 1;
exit when E_Strings.Get_Element (E_Str => Line,
Pos => Next_Pos) = ' ';
end loop;
return Next_Pos;
end Find_Next_Space;
begin
if End_Pos = 0 then
Current_Line_End := E_Strings.Get_Length (E_Str => Line);
else
Current_Space_Pos := Find_Next_Space (Curr_Pos => Current_Line_Pos);
loop
exit when Current_Space_Pos = E_Strings.Get_Length (E_Str => Line);
Next_Space_Pos := Find_Next_Space (Curr_Pos => Current_Space_Pos);
exit when (Pos + Next_Space_Pos) - Current_Line_Start >= End_Pos;
Current_Space_Pos := Next_Space_Pos;
end loop;
Current_Line_End := Current_Space_Pos;
end if;
end Find_Current_Line_End;
begin
Current_Line_Start := 1;
Pos := Start_Pos;
Find_Current_Line_End (Current_Line_Pos => 0);
loop
Print_Current_Line;
exit when Current_Line_End = E_Strings.Get_Length (E_Str => Line);
Put_Spaces (File => Listing,
N => Indent);
Pos := Indent;
Current_Line_Start := Current_Line_End + 1;
Find_Current_Line_End (Current_Line_Pos => Current_Line_Start);
end loop;
New_Start := Pos + ((Current_Line_End + 1) - Current_Line_Start);
end PrintLine;
|
