1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT RUN-TIME COMPONENTS                         --
4--                                                                          --
5--                     ADA.STRINGS.TEXT_BUFFERS.BOUNDED                     --
6--                                                                          --
7--                                 S p e c                                  --
8--                                                                          --
9--            Copyright (C) 2020-2021, Free Software Foundation, Inc.       --
10--                                                                          --
11-- This specification is derived from the Ada Reference Manual for use with --
12-- GNAT.  In accordance with the copyright of that document, you can freely --
13-- copy and modify this specification,  provided that if you redistribute a --
14-- modified version,  any changes that you have made are clearly indicated. --
15--                                                                          --
16------------------------------------------------------------------------------
17
18package Ada.Strings.Text_Buffers.Bounded with
19   Pure
20is
21
22   type Buffer_Type (Max_Characters : Text_Buffer_Count) is
23     new Root_Buffer_Type with private with
24      Default_Initial_Condition => not Text_Truncated (Buffer_Type);
25
26   function Text_Truncated (Buffer : Buffer_Type) return Boolean;
27
28   function Get (Buffer : in out Buffer_Type) return String with
29      Post'Class => Get'Result'First = 1 and then Current_Indent (Buffer) = 0;
30
31   function Wide_Get (Buffer : in out Buffer_Type) return Wide_String with
32      Post'Class => Wide_Get'Result'First = 1
33      and then Current_Indent (Buffer) = 0;
34
35   function Wide_Wide_Get
36     (Buffer : in out Buffer_Type) return Wide_Wide_String with
37      Post'Class => Wide_Wide_Get'Result'First = 1
38      and then Current_Indent (Buffer) = 0;
39
40   function Get_UTF_8
41     (Buffer : in out Buffer_Type) return UTF_Encoding.UTF_8_String with
42      Post'Class => Get_UTF_8'Result'First = 1
43      and then Current_Indent (Buffer) = 0;
44
45   function Wide_Get_UTF_16
46     (Buffer : in out Buffer_Type) return UTF_Encoding.UTF_16_Wide_String with
47      Post'Class => Wide_Get_UTF_16'Result'First = 1
48      and then Current_Indent (Buffer) = 0;
49
50private
51
52   procedure Put_UTF_8_Implementation
53     (Buffer : in out Root_Buffer_Type'Class;
54      Item   : UTF_Encoding.UTF_8_String)
55     with Pre => Buffer in Buffer_Type'Class;
56
57   package Mapping is new Output_Mapping (Put_UTF_8_Implementation);
58
59   subtype Positive_Text_Buffer_Count is
60     Text_Buffer_Count range 1 .. Text_Buffer_Count'Last;
61
62   type Convertible_To_UTF_8_String is
63     array (Positive_Text_Buffer_Count range <>) of Character;
64
65   type Buffer_Type (Max_Characters : Text_Buffer_Count)
66   is new Mapping.Buffer_Type with record
67      Truncated : Boolean := False;
68      --  True if we ran out of space on a Put
69
70      Chars : Convertible_To_UTF_8_String (1 .. Max_Characters);
71   end record;
72
73end Ada.Strings.Text_Buffers.Bounded;
74