History log of /seL4-l4v-10.1.1/HOL4/src/parse/term_pp_utils.sml
Revision Date Author Comments
# fea9bc14 14-Mar-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Now up to Parse.sml


# b847c215 01-Aug-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Extract pretty-printing of LET-terms from term_pp.sml

It is now part of user-printer "land" in src/bool/boolpp.sml,
alongside the custom printer for if-then-else (COND).

This refactoring revealed a bug in the way overloaded constants
couldn't be handled by user-printers if they could have extra
arguments hanging off to the right (as in “LET f x y”), *unless* they
were overloaded to "case" (as in COND).

To make sure one's user-printer is going to work, you have to consult
the grammar's overload information to check if your term is one you
want to print according to the grammar_name function. Unfortunately,
looking for particular constants is not guaranteed to work, as the
process of descending terms in the pretty-printer is liable to turn
real constants into special "fake" constants that are actually
variables with special names.

This is progress with Github issue #154, to allow new (Isabelle-style)
syntax for let expressions.


# e83cfa48 27-Sep-2011 Michael Norrish <Michael.Norrish@nicta.com.au>

Make case-expressions in set comprehensions print with parentheses.

The way this is made to work is rather hackish: every possible case
expression in a comprehension gets parenthesised, even if it won't
cause a parse error. I don't expect there are many such in any case.


# a4acbc77 06-Jan-2011 Michael Norrish <Michael.Norrish@nicta.com.au>

Significant change to pretty-printing; affects user-printing API.

The change allows user-printers to alter the main printer's notion of
what is a "seen free variable", and what is bound. The latter causes
the colouring. The first notion is important when show_types is on,
as types are only given for the first occurrence of a free variable.

This allows the monadsyntax to do the right thing with the colouring
of variables.