		Search-engine friendly clone of the ACL2 documentation.

Printer

Printing-locally

How to use ps to build strings in a local context.

A disadvantage of using a stobj to represent the printer's state is that it is generally non-instantiable, which makes localized string building more difficult because printing from one function may interfere with printing from another.

We provide two mechanisms for coping with this.

The recommended approach is to use with-local-ps, which in turn uses with-local-stobj to give you a temporary ps to work with.

An alternative, which we do not often use, is to explicitly manage saving and restoring of the printer's state. To support this, we provide some routines for saving and restoring configurations, and for resetting the printer's fields.

Subtopics

Vl-psconfig-p: Configuration object for saving and loading printer state.
Vl-ps-full-reset: Erase all contents and reset ps to its default configuration.
Vl-ps-save-config: Save the current configuration of ps into a vl-psconfig-p object.
Vl-ps-load-config: Load configuration settings from a vl-psconfig-p object into ps.
Vl-ps-text-reset: Erase the contents of ps without altering its configuration.
With-local-ps: Print using a local instance of ps.