class interface STD_FILE_WRITE
   -- 
   --  Basic output facilities to write a named file on the disk.
   -- 
   --  Note : most features are common with STD_OUTPUT so you can 
   --         test your program first on the screen and then, changing 
   --         of instance (STD_OUTPUT/STD_FILE_WRITE), doing the same
   --         on a file.
   -- 

creation
   connect_to (new_path: STRING)
      require
         not is_connected;
         not new_path.empty

   make

feature(s) from OUTPUT_STREAM
   --  State of the stream :

   is_connected: BOOLEAN

feature(s) from OUTPUT_STREAM
   --  To write one character at a time :

   put_character (c: CHARACTER)
      require
         is_connected

feature(s) from OUTPUT_STREAM
   put_string (s: STRING)
      --  Output s to current output device.

      require
         is_connected;
         s /= Void

feature(s) from OUTPUT_STREAM
   --  To write a number :

   put_integer (i: INTEGER)
      --  Output i to current output device.

      require
         is_connected

   put_integer_format (i, s: INTEGER)
      --  Output i to current output device using at most
      --  s character.

      require
         is_connected

   put_real (r: REAL)
      --  Output r to current output device.

      require
         is_connected

   put_real_format (r: REAL; f: INTEGER)
      --  Output r with only f digit for the fractionnal part.
      --  Examples: 
      --     put_real(3.519,2) print "3.51".

      require
         is_connected;
         f >= 0

   put_double (d: DOUBLE)
      --  Output d to current output device.

      require
         is_connected

   put_double_format (d: DOUBLE; f: INTEGER)
      --  Output d with only f digit for the fractionnal part.
      --  Examples: 
      --     put_double(3.519,2) print "3.51". 

      require
         is_connected;
         f >= 0

feature(s) from OUTPUT_STREAM
   --  Other features :   

   put_boolean (b: BOOLEAN)
      --  Output b to current output device according
      --  to the Eiffel format.

      require
         is_connected

   put_pointer (p: POINTER)
      --  Output a viewable version of p.

      require
         is_connected

   put_new_line
      --  Output a newline character.

      require
         is_connected

   put_spaces (nb: INTEGER)
      --  Output nb spaces character.

      require
         nb >= 0

   append_file (file_name: STRING)
      require
         is_connected;
         file_exists(file_name)

   flush

feature(s) from STD_FILE_WRITE
   path: STRING
      --  Not Void when connected to the corresponding file
      --  on the disk.


feature(s) from STD_FILE_WRITE
   connect_to (new_path: STRING)
      require
         not is_connected;
         not new_path.empty

feature(s) from STD_FILE_WRITE
   disconnect
      require
         is_connected

   make


end of STD_FILE_WRITE