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()