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