#
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.
|
#
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.
|