Parse.rawterm

STRUCTURE

SYNOPSIS

Causes a function to use the raw terminal backend when pretty-printing.

DESCRIPTION

Functions that pretty-print HOL types, terms and theorems do so through an abstraction called a “backend”. Using these backends allows output to be customised to the facilities provided by different display devices. For example, on terminals supporting DEC’s vt100 colour coding, free variables are displayed in blue. There is also a “raw terminal” backend, that doesn’t change the output in any way.

When an interactive session begins, HOL links all of the pretty-printing functions to a backend value stored in a reference, Parse.current_backend. Of course, this reference can be changed as a user desires. A call to rawterm_pp f function wraps a call to Lib.with_flag, setting the current backend to be the raw terminal value for the duration of the f’s application to its (first) argument.

FAILURE

A call to rawterm_pp f never fails. A call to rawterm_pp f x should only fail if f x would fail, but this ultimately depends on f’s implementation.

EXAMPLE

In a vt100-compatible terminal, capturing the output of pp_term reveals a stream of horrible-looking escape codes:

   > ppstring pp_term ``p /\ q``;
   val it = "\^[[0;1;34mp\^[[0m /\\ \^[[0;1;34mq\^[[0m": string

If this string is to be print-ed to the vt100, it will colour the p and q a pleasant blue colour. If, on the other hand, the string is to be output to a file, the colouring is probably not desirable. Then one can use rawterm_pp to get the unadorned characters of the output:

   > rawterm_pp (ppstring pp_term) ``p /\ q``;
   val it = "p /\\ q": string

This last usage is so common that it is already available in the library as term_to_string.

COMMENTS

If a function f is curried with multiple arguments, say f x y, then care will probably be needed with modifying it with rawterm_pp. In particular, rawterm_pp f x y is likely not to work, while rawterm_pp (f x) y probably will.

SEEALSO

ppstring, term_to_string, with_flag