[isabelle-dev] Isabelle_12-Sep-2013

[Makarius]

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