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
|
-------------------------------------------------------------------------------
-- (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.
--
--=============================================================================
with E_Strings;
--# inherit Ada.Characters.Handling,
--# Ada.Characters.Latin_1,
--# CommandLineData,
--# ExaminerConstants,
--# E_Strings,
--# FileSystem,
--# ScreenEcho,
--# SPARK_IO;
package CommandLineHandler is
type Command_Strings is record
Current_Position : E_Strings.Positions;
Contents : E_Strings.T;
end record;
type S_Typs is (S_Empty,
S_Equal,
S_Switch_Character,
S_Comma,
S_String,
S_Continue);
type Symbols is record
Typ : S_Typs;
The_String : E_Strings.T;
end record;
function Check_Option_Name (Opt_Name : E_Strings.T;
Str : String) return Boolean;
procedure Skip_Spaces (Command_String : in out Command_Strings);
--# derives Command_String from *;
procedure Read_The_String (Command_String : in out Command_Strings;
Next_Symbol : in out Symbols);
--# derives Command_String,
--# Next_Symbol from *,
--# Command_String;
----------------------------------------------------------------------------
-- Reads the default switch file "spark.sw", then the user's
-- command-line switches. Parses these and sets the content
-- of CommandLineData.Content appropriately. Illegal or
-- contradictory switches are detected and reported.
--
-- As a special case, if -noswitch has been given on the command-line,
-- then the default switch file "spark.sw" is completely ignored.
----------------------------------------------------------------------------
procedure Process;
--# global in out CommandLineData.Content;
--# in out SPARK_IO.File_Sys;
--# derives CommandLineData.Content,
--# SPARK_IO.File_Sys from CommandLineData.Content,
--# SPARK_IO.File_Sys;
----------------------------------------------------------------------------
-- Reads and parses the default switch file, setting
-- CommandLineData.Content as it goes, but doesn't
-- check for existence or non-overlapping of
-- input files. Used by tools like SPARKFormat
-- which want to be able to read the default switch
-- file, but don't care if the index file(s) (and so on)
-- don't actually exist.
--
-- As a special case, if -noswitch has been given on the command-line,
-- then the default switch file "spark.sw" is completely ignored.
----------------------------------------------------------------------------
procedure Process_Defaults_From_Switch_File;
--# global in out CommandLineData.Content;
--# in out SPARK_IO.File_Sys;
--# derives CommandLineData.Content,
--# SPARK_IO.File_Sys from CommandLineData.Content,
--# SPARK_IO.File_Sys;
end CommandLineHandler;
|
