[Ada] Update the documentation of functional containers

[Ada] Update the documentation of functional containers

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 263 bytes --]

Functional containers are now controlled. Update the documentation
accordingly.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* doc/gnat_rm/the_gnat_library.rst: Functional vectors, sets,
	and maps are now controlled.
	* gnat_rm.texi: Regenerate.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 7320 bytes --]

diff --git a/gcc/ada/doc/gnat_rm/the_gnat_library.rst b/gcc/ada/doc/gnat_rm/the_gnat_library.rst
--- a/gcc/ada/doc/gnat_rm/the_gnat_library.rst
+++ b/gcc/ada/doc/gnat_rm/the_gnat_library.rst
@@ -285,17 +285,16 @@ specification of this unit is compatible with SPARK 2014.
 .. index:: Functional sets
 
 This child of ``Ada.Containers`` defines immutable sets. These containers are
-unbounded and may contain indefinite elements. Furthermore, to be usable in
-every context, they are neither controlled nor limited. As they are functional,
-that is, no primitives are provided which would allow modifying an existing
-container, these containers can still be used safely.
+unbounded and may contain indefinite elements. Their API features functions
+creating new containers from existing ones. To remain reasonably efficient,
+their implementation involves sharing between data-structures. As they are
+functional, that is, no primitives are provided which would allow modifying an
+existing container, these containers can still be used safely.
 
-Their API features functions creating new containers from existing ones.
-As a consequence, these containers are highly inefficient. They are also
-memory consuming, as the allocated memory is not reclaimed when the container
-is no longer referenced. Thus, they should in general be used in ghost code
-and annotations, so that they can be removed from the final executable. The
-specification of this unit is compatible with SPARK 2014.
+These containers are controlled so that the allocated memory can be reclaimed
+when the container is no longer referenced. Thus, they cannot directly be used
+in contexts where controlled types are not supported.
+The specification of this unit is compatible with SPARK 2014.
 
 .. _`Ada.Containers.Functional_Maps_(a-cofuma.ads)`:
 
@@ -307,17 +306,16 @@ specification of this unit is compatible with SPARK 2014.
 .. index:: Functional maps
 
 This child of ``Ada.Containers`` defines immutable maps. These containers are
-unbounded and may contain indefinite elements. Furthermore, to be usable in
-every context, they are neither controlled nor limited. As they are functional,
-that is, no primitives are provided which would allow modifying an existing
-container, these containers can still be used safely.
-
-Their API features functions creating new containers from existing ones.
-As a consequence, these containers are highly inefficient. They are also
-memory consuming, as the allocated memory is not reclaimed when the container
-is no longer referenced. Thus, they should in general be used in ghost code
-and annotations, so that they can be removed from the final executable. The
-specification of this unit is compatible with SPARK 2014.
+unbounded and may contain indefinite elements. Their API features functions
+creating new containers from existing ones. To remain reasonably efficient,
+their implementation involves sharing between data-structures. As they are
+functional, that is, no primitives are provided which would allow modifying an
+existing container, these containers can still be used safely.
+
+These containers are controlled so that the allocated memory can be reclaimed
+when the container is no longer referenced. Thus, they cannot directly be used
+in contexts where controlled types are not supported.
+The specification of this unit is compatible with SPARK 2014.
 
 .. _`Ada.Containers.Bounded_Holders_(a-coboho.ads)`:
 


diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -23520,17 +23520,16 @@ specification of this unit is compatible with SPARK 2014.
 @geindex Functional sets
 
 This child of @code{Ada.Containers} defines immutable sets. These containers are
-unbounded and may contain indefinite elements. Furthermore, to be usable in
-every context, they are neither controlled nor limited. As they are functional,
-that is, no primitives are provided which would allow modifying an existing
-container, these containers can still be used safely.
+unbounded and may contain indefinite elements. Their API features functions
+creating new containers from existing ones. To remain reasonably efficient,
+their implementation involves sharing between data-structures. As they are
+functional, that is, no primitives are provided which would allow modifying an
+existing container, these containers can still be used safely.
 
-Their API features functions creating new containers from existing ones.
-As a consequence, these containers are highly inefficient. They are also
-memory consuming, as the allocated memory is not reclaimed when the container
-is no longer referenced. Thus, they should in general be used in ghost code
-and annotations, so that they can be removed from the final executable. The
-specification of this unit is compatible with SPARK 2014.
+These containers are controlled so that the allocated memory can be reclaimed
+when the container is no longer referenced. Thus, they cannot directly be used
+in contexts where controlled types are not supported.
+The specification of this unit is compatible with SPARK 2014.
 
 @node Ada Containers Functional_Maps a-cofuma ads,Ada Containers Bounded_Holders a-coboho ads,Ada Containers Functional_Sets a-cofuse ads,The GNAT Library
 @anchor{gnat_rm/the_gnat_library ada-containers-functional-maps-a-cofuma-ads}@anchor{2f4}@anchor{gnat_rm/the_gnat_library id16}@anchor{2f5}
@@ -23542,17 +23541,16 @@ specification of this unit is compatible with SPARK 2014.
 @geindex Functional maps
 
 This child of @code{Ada.Containers} defines immutable maps. These containers are
-unbounded and may contain indefinite elements. Furthermore, to be usable in
-every context, they are neither controlled nor limited. As they are functional,
-that is, no primitives are provided which would allow modifying an existing
-container, these containers can still be used safely.
-
-Their API features functions creating new containers from existing ones.
-As a consequence, these containers are highly inefficient. They are also
-memory consuming, as the allocated memory is not reclaimed when the container
-is no longer referenced. Thus, they should in general be used in ghost code
-and annotations, so that they can be removed from the final executable. The
-specification of this unit is compatible with SPARK 2014.
+unbounded and may contain indefinite elements. Their API features functions
+creating new containers from existing ones. To remain reasonably efficient,
+their implementation involves sharing between data-structures. As they are
+functional, that is, no primitives are provided which would allow modifying an
+existing container, these containers can still be used safely.
+
+These containers are controlled so that the allocated memory can be reclaimed
+when the container is no longer referenced. Thus, they cannot directly be used
+in contexts where controlled types are not supported.
+The specification of this unit is compatible with SPARK 2014.
 
 @node Ada Containers Bounded_Holders a-coboho ads,Ada Command_Line Environment a-colien ads,Ada Containers Functional_Maps a-cofuma ads,The GNAT Library
 @anchor{gnat_rm/the_gnat_library ada-containers-bounded-holders-a-coboho-ads}@anchor{2f6}@anchor{gnat_rm/the_gnat_library id17}@anchor{2f7}