SPARK examiner visibility problem

[Laurie Dillon <lauradillo@gmail.com>]

I am having trouble with a toy example of encapsulating IO for a SPARK
program.  My example seems to be consistent with the Spark_IO example
in the Barnes book.

I have the following package spec:

-------------------------------------------------------------------------------------

with Ada.Text_IO;
package Std_IO
--  encapsulates IO to and from standard input and standard output
--# own stdin: Istream_Type;
--#        stdout: Ostream_Type;
--# initializes stdin,
--#                 stdout;
is
   --# type Istream_Type is abstract;
   --# type Ostream_Type is abstract;

   procedure New_Line;
   --  output a new line to stdout
   --# global in out stdout;
   --# derives stdout from *;

   procedure Put_Line (Item  : in String);
   --  output a string followed by a carriage return to stdout
   --# global in out stdout;
   --# derives stdout from *, Item;

   procedure Put_Integer (Item : in Integer);
   --  output an integer to stdout
   --# global in out stdout;
   --# derives stdout from *, Item;

   procedure Get_Integer (Item : out Integer;
                          OK   : out Boolean);
   --  input an integer from stdin
   --# global in stdin;
   --# derives Item, OK from stdin;

end Std_IO;
----------------------------------------------------------------------------------------------------------

The examiner has no problem with this package (the body carries a
#hide Std_IO annotation).  But when I try to examine a package spec
(or body) that inherits Std_IO, I get semantic errors at every
reference to Std_IO.stdin and Std_IO.stdout.

For example, consider the following spec:
-----------------------------------------------------------------------------------
--# inherit Std_IO;
package MyGps
--# own home;
is

   type Location is
   record
      x : Integer;
      y : Integer;
   end record;

   procedure MoveTo (theLoc : in Location);
   --  moves home to the given location
   --# global out home;
   --# derives home from theLoc;

   function Distance (theLoc : Location) return Integer;
   --  returns the (taxi) distance from home to the given location
   --# global home;

   procedure GetLocation (theLoc : out Location);
   --  prompts user for theLoc
   --# derives theLoc from Std_IO.stdin;

end MyGps;
---------------------------------------------------------------------------------------------
Examiner report says:

   Unit name:  MyGps
   Unit type:  package specification
   Unit has been analysed, any errors are listed below.

1 error(s) or warning(s)

Line
  23     --# derives theLoc from Std_IO.stdin;
                                 ^1
*** (  1)  Semantic Error    :752: The identifier Std_IO.stdin is
either undeclared
           or not visible at this point. This identifier must appear
in a
           preceding legal global annotation or formal parameter list.
-------------------------------------------------------------------------------------

I thought the own declaration for stdin in the spec of Spark_IO should
qualify as "a preceding legal global annotation".   What am I missing
here?

Analysis of the body of myGps gives similar errors.  For example:

   Unit name:  MyGps
   Unit type:  package body
   Unit has been analysed, any errors are listed below.

14 error(s) or warning(s)

Line
  35        Std_IO.Put_Line (Item => "Enter x-coordinate of location :
");
            ^1,2
*** (  1)  Semantic Error    : 25: The identifier Std_IO.stdout
(imported by called
           subprogram) is not visible at this point.
*** (  2)  Semantic Error    : 24: The identifier Std_IO.stdout
(exported by called
           subprogram) is not visible at this point.
--------------------------------------------------------------------------------------

Note that Std_IO.Put_Line is visible, as it should be.

Any insights or explanation for what I'm doing wrong in this example
will be greatly appreciated!

Thanks,

Laurie