rawterm_ppParse.rawterm_pp : ('a -> 'b) -> 'a -> 'bCauses a function to use the raw terminal backend when pretty-printing.
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.
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.
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": stringIf 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": stringThis last usage is so common that it is already available in the
library as term_to_string.
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.