class interface KL_OUTPUT_STREAM_ROUTINES

feature(s) from KL_IMPORTED_OUTPUT_STREAM_ROUTINES
   --  Access

   OUTPUT_STREAM_: KL_OUTPUT_STREAM_ROUTINES
      --  Routines that ought to be in class OUTPUT_STREAM

      ensure
         output_stream_routines_not_void: Result /= Void

feature(s) from KL_IMPORTED_OUTPUT_STREAM_ROUTINES
   --  Type anchors

   OUTPUT_STREAM_TYPE: OUTPUT_STREAM

feature(s) from KL_OUTPUT_STREAM_ROUTINES
   --  Initialization

   make_file_open_write (a_filename: STRING): like OUTPUT_STREAM_TYPE
      --  Create a new file object with a_filename as
      --  file name and try to open it in write-only mode.
      --  is_open_write (Result) is set to True
      --  if operation was successful.

      require
         a_filename_not_void: a_filename /= Void;
         a_filename_not_empty: a_filename.count > 0
      ensure
         file_not_void: Result /= Void

feature(s) from KL_OUTPUT_STREAM_ROUTINES
   --  Status report

   is_open_write (a_stream: like OUTPUT_STREAM_TYPE): BOOLEAN
      --  Is a_stream open in write mode?

      require
         a_stream_void: a_stream /= Void

   is_closed (a_stream: like OUTPUT_STREAM_TYPE): BOOLEAN
      --  Is a_stream closed?

      require
         a_stream_void: a_stream /= Void

feature(s) from KL_OUTPUT_STREAM_ROUTINES
   --  Status setting

   close (a_stream: like OUTPUT_STREAM_TYPE)
      --  Close a_stream if it is closable,
      --  let it open otherwise.

      require
         a_stream_not_void: a_stream /= Void;
         not_closed: not is_closed(a_stream)


end of KL_OUTPUT_STREAM_ROUTINES