Subject: System

Keywords: ::tips
          ::usage

Title: print output

--------------------------------------------------

Refinements run on arbitrary machines which do not have access
to home directories. Therefore print output must go to the shared
/usr/nuprl/public path.

The function with_tty_file will redirect ouput to /usr/nuprl/public/tmp/tty :
with_tty_file : bool -> string -> (* -> **) -> * -> **
  bool : append if true, overwrite if false 
  string : a relative pathname.
    - For example, tty_print false mydir/foobar will overwrite file
      /usr/nuprl/public/tmp/tty/mydir/foobar.
    - Any directories in pathname must exist, they will not be created.
      If a directory does not exist with_tty_file will fail.
    - The file however will be created if it does not exist.

Objects printed from obid collector may go to /usr/nuprl/public/tmp.

The editor, however, should have access to the users home directory.
In the editor by default, the function, theory_prefix: unit -> string,
returns the path /home/<user>/nuprlprint.
Navigator buttons which cause theory content to be printed by the editor
will go to that path.  
⋅
--------------------------------------------------

Authors: 

Contributors: NUPRL:t
              RICH:t

⋅

Home