1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT RUN-TIME COMPONENTS                         --
4--                                                                          --
5--                 A D A . T E X T _ I O . F I X E D _ I O                  --
6--                                                                          --
7--                                 S p e c                                  --
8--                                                                          --
9-- This specification is derived from the Ada Reference Manual for use with --
10-- GNAT.  In accordance with the copyright of that document, you can freely --
11-- copy and modify this specification,  provided that if you redistribute a --
12-- modified version,  any changes that you have made are clearly indicated. --
13--                                                                          --
14------------------------------------------------------------------------------
15
16--  In Ada 95, the package Ada.Text_IO.Fixed_IO is a subpackage of Text_IO.
17--  This is for compatibility with Ada 83. In GNAT we make it a child package
18--  to avoid loading the necessary code if Fixed_IO is not instantiated. See
19--  routine Rtsfind.Check_Text_IO_Special_Unit for a description of how we
20--  patch up the difference in semantics so that it is invisible to the Ada
21--  programmer.
22
23private generic
24   type Num is delta <>;
25
26package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is
27
28   Default_Fore : Field := Num'Fore;
29   Default_Aft  : Field := Num'Aft;
30   Default_Exp  : Field := 0;
31
32   procedure Get
33     (File  : File_Type;
34      Item  : out Num;
35      Width : Field := 0)
36   with
37     Pre    => Is_Open (File) and then Mode (File) = In_File,
38     Global => (In_Out => File_System);
39
40   procedure Get
41     (Item  : out Num;
42      Width : Field := 0)
43   with
44     Post   =>
45       Line_Length'Old = Line_Length
46       and Page_Length'Old = Page_Length,
47     Global => (In_Out => File_System);
48
49   procedure Put
50     (File : File_Type;
51      Item : Num;
52      Fore : Field := Default_Fore;
53      Aft  : Field := Default_Aft;
54      Exp  : Field := Default_Exp)
55   with
56     Pre    => Is_Open (File) and then Mode (File) /= In_File,
57     Post   =>
58       Line_Length (File)'Old = Line_Length (File)
59       and Page_Length (File)'Old = Page_Length (File),
60     Global => (In_Out => File_System);
61
62   procedure Put
63     (Item : Num;
64      Fore : Field := Default_Fore;
65      Aft  : Field := Default_Aft;
66      Exp  : Field := Default_Exp)
67   with
68     Post   =>
69       Line_Length'Old = Line_Length
70       and Page_Length'Old = Page_Length,
71     Global => (In_Out => File_System);
72
73   procedure Get
74     (From : String;
75      Item : out Num;
76      Last : out Positive)
77   with
78     Global => null;
79
80   procedure Put
81     (To   : out String;
82      Item : Num;
83      Aft  : Field := Default_Aft;
84      Exp  : Field := Default_Exp)
85   with
86     Global => null;
87
88private
89   pragma Inline (Get);
90   pragma Inline (Put);
91
92end Ada.Text_IO.Fixed_IO;
93