Nuprl - How to Print Collections of Nuprl Objects

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

How to Print Collections of Nuprl Objects

To prepare a Latex article from Nuprl objects see MakingLatexArticles. Here we describe a way of making listings, still using Latex, that are less attractive than that Article-making method, but are more likely to work in reproducing the on-line appearance of Nuprl objects and producing a readable form for any object. Multiple objects printed together will also be cross referenced. The article method will be gradually enhanced to subsume more of these generic object printing features, but for now the methods described below are still needed for getting practical paper versions of Nuprl objects generally without need of tailoring for an Article format.

The button PrintObSet in the I/O Menu is presents a good rough-and-ready method suitable for many work-a-day purposes.

PRINTobs
page width      : 80
filepath(no ext): W"[word]"
show pf when    : (ob:tok. false |true)
obs to print    : [<ml>]:tok list

Here the file path should be the directory path plus the filname rootname to be used for the various files, which will be extended to ".text", ".tex" et cetera. A bit more tailoring is possible with

print_ob_set_to_file_std printwidth:int multipart:bool,pathname:string
pf_is_displayed:tokbool
printobs:tok list

where:

printwidth is the number of characters permitted per line.

multipart indicates whether an index to the objects is to be created (a separate file named INDEX).

pathname If multipart=true then pathname should be a directory where the index and the one-or-more sections will be output.
If multipart=false then pathname should be the directory path plus the filname rootname to be used for the various files (which will be extended to ".text", ".tex" etc).

pf_is_displayed is a function applied to THM objects indicating for each whether its proof is to be printed rather than just the theorem statement; note that if a theorem is listed more than once then all but the last will be printed as theorem statement only.

printobs is the list of objects to be printed.

Using print_ob_set_to_file_verbatim instead of print_ob_set_to_file_std avoids several standard conversions of terms giving a truer, if sometimes more ambiguous, static rendering of the object contents. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

EditorDoc Sections Nuprl Doc

printwidth	is the number of characters permitted per line.

multipart	indicates whether an index to the objects is to be created (a separate file named INDEX).

pathname	If multipart=true then pathname should be a directory where the index and the one-or-more sections will be output. If multipart=false then pathname should be the directory path plus the filname rootname to be used for the various files (which will be extended to ".text", ".tex" etc).

pf_is_displayed	is a function applied to THM objects indicating for each whether its proof is to be printed rather than just the theorem statement; note that if a theorem is listed more than once then all but the last will be printed as theorem statement only.

printobs	is the list of objects to be printed.