class interface PYTHON_FILE
creation
make_from_borrowed_reference (new_python_object_pointer: POINTER)
-- uses the given object pointer and increases the reference
-- count of the given python object. Used in cases where the
-- Python C api does not automatically increase the reference
-- count. Terminology ("borrowed reference" vs "new reference")
-- is taken from the Python C Api documentation
require
new_python_object_pointer.is_not_null
make_from_filename (filename, mode: STRING)
-- opens the file with the given filename
make_from_python_object (object: PYTHON_OBJECT)
-- uses the existing python_object_pointer of python_object
require
object /= Void
feature(s) from PYTHON_FILE
make_from_filename (filename, mode: STRING)
-- opens the file with the given filename
get_line (num_chars: INTEGER): PYTHON_STRING
-- like p.readline( [n] ) from python--see python documentation
file_name: PYTHON_STRING
-- name of the open file
set_buffer_size (new_size: INTEGER)
-- sets the buffer size--python PyFile_SetBufSize
write_object (object: PYTHON_OBJECT)
-- writes the given object to the file. The C function
-- interface accepts a "flags" argument, but at the moment
-- the only flag supported is "Py_PRINT_RAW", so that's
-- hardcoded for now
ensure
last_python_integer_result_ok
write_string (string: STRING)
-- writes the given string to the file
ensure
last_python_integer_result_ok
invariant
reference_count >= 0;
valid_reference: not is_none implies is_file;
end of PYTHON_FILE |