[m-dev.] pretty vs raw_pretty

[Ian MacLarty]

In mdb I think the "raw_pretty" browser format is a lot prettier than 
the "pretty" format, especially when printing maps and lists.

Does anyone feel the same way?

I propose swapping the two format names, so "raw_pretty" would become 
"pretty" and "pretty" would become "raw_pretty".

I suspect a few test expected outputs will need to change, but I don't 
mind doing this.

Ian.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------