[m-dev.] pretty vs raw_pretty
Ralph Becket
rafe at cs.mu.OZ.AU
Thu Nov 4 16:09:03 AEDT 2004
Ian MacLarty, Thursday, 4 November 2004:
> 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.
IIRC, "pretty" did mean "raw_pretty", but was renamed by a summer
student who wanted "pretty" for a far more raw printing option of his
own :-)
I imagine we could even remove the less pretty pretty-printer
altogether. It would be better to have just one and develop that as
required.
-- Ralph
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the developers
mailing list