On Fri, 13 Sep 2013, David Greenaway wrote:
For example, trying to view the current progress of the command:
ML {*
map (fn x => (tracing (PolyML.makestring x);
OS.Process.sleep (seconds 0.1))) (1 upto 100)
*}
is difficult.
I will look at the other observations in due time.
For above, just again a reminder that PolyML.makestring is inappropriate
for regular Isabelle/ML usage. The documented @{make_string}
antiquotation works better.
I am, of course, happy to submit patches for review for any (or all) of
these problems if there is any indication that such patches would be
appreciated.
No, not again this waste of time.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
