SCRIBELIBFILE : LIBRARYCMD

SCRIBELIBFILE is a library command.
Print the specified library files into MSS files.
The three verbosity settings are: MIN, which just shows the names of the
objects, MED, which shows the help messages, keywords, provability and wffs
as well, and MAX, which shows everything. It can take a list of filenames and
a corresponding list of output files; if the latter list is too long it will
be truncated, and if it is too short then the last filename given will be used
for all the remaining output (so you can write a group of library files to a
single output file by only supplying one output filename).
After leaving TPS, run the .mss files through Scribe and print the resulting
files.

Some files in the list of library files may be ambiguous, in the
sense that more than one file of the given name exists in the
library directories in DEFAULT-LIB-DIR and BACKUP-LIB-DIR.
In this case, the user is prompted to disambiguate each ambiguous
filename from first to last.
 
The command format for SCRIBELIBFILE is:

<LIB>SCRIBELIBFILE FILENAMESIN FILENAMESOUT VERBOSITY
"FILESPECLIST" "FILESPECLIST" "SYMBOL"

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage