File

File -- the class of all files.

Files may be input files, output files, pipes, or sockets. The class of all files is File.

Some standard files, already open:

  • stdio -- standard input output file
  • stderr -- standard error output file

    • Ways to create new files:

  • openIn -- open an input file
  • openOut -- open an output file
  • openInOut -- open an input output file
  • openListener -- open a listener

    • Ways to change the state of files:

  • echoOff -- set echoing off
  • echoOn -- set echoing on

    • Input operations:

  • getc -- get one character from a file
  • get -- get contents of a file
  • read -- get some bytes from a file
  • atEndOfFile -- whether the file is at the end
  • isReady -- whether data is available from a file, or it's at the end

    • Further processing for data obtained from a file:

  • lines -- split a string into lines

    • Output operations:

  • << -- print to file
  • endl -- end a line
  • flush -- flush a file
  • printString -- print a generalized string
  • print -- print an expression on a line
  • TeX -- call TeX to display an expression

    • Preparing expressions for output:

  • columnate
  • expression
  • format
  • name
  • null -- a symbol which doesn't print
  • pad
  • string
  • tex
  • toString

    • Destroying files:

  • close -- close a file
  • closeIn -- close a file for input
  • closeOut -- close a file for output
  • kill -- kill a process associated with a file

    • Information about files

  • width -- width of a terminal
  • openFiles -- list open files
  • isOpenFile -- whether it's an open file
  • isInputFile -- whether it's an input file
  • isOutputFile -- whether it's an output file
  • isListener -- whether it's a listener

    • topindexpreviousupnext