Re: [isabelle] make_string





On 21/06/18 05:46, Makarius wrote:
On 20/06/18 15:04, Jeremy Dawson wrote:

Thanks for the information that I shouldn't be using @{make_string}.
This raises the obvious question of what I should be using.  Would it be
possible for you to tell me that?  Ie, what is the equivalent in the
managed ML environment called "Isabelle/ML" of the PolyML function
PolyML.makestring?

There is none. For quick adhoc debugging and diagnistics, there is
@{print} and @{make_string}. For production-quality output, you do it
yourself specifically for your data types, potentially using existing
operations like Syntax.pretty_term -- generally it is better to print
Pretty.T than string.


	Makarius


Well, obviously I don't want to create a print function for any new datatype when there is one there already (now that I've been told how to remove all the extra crap in the output from @{make_string}).

In what way is @{make_string} not suitable for production-quality output?

Thanks

Jeremy




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.