close - close an open File
file.close()
file.close(disp)
Because of the tight coupling of operating system interactions,
there is no implicit memory management of File
handles, so they must be closed explicitly using the
close()
intrinsic method. The optional string
disp may be provided. Currently, the only supported
disp string is "delete", which specifies that the
file should be deleted after it is closed.
None
TypeCheck
if file is not a
File
or disp is not a string
RangeCheck
if disp is provided and is not
"delete"
AccessCheck
if
file has already been closed
f = new File("hello.txt", "w") f.say("Hello!\n") f.close()