[m-dev.] pretty vs raw_pretty

[Ian MacLarty]

On 4 Nov 2004, at 16:09, Ralph Becket wrote:

> 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.
>
I'll just rename them for now.  The raw_pretty option doesn't appear to 
be documented in the online help or the user guide, so by renaming them 
I'd effectively be removing the current "pretty" format.  This okay?

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