Re: [isabelle] Isabelle2016-RC2 JEdit lockup with Java at 100% CPU (was: Re: Isabelle2016-RC2 Java exceptions related to search/replace)

On Sun, 31 Jan 2016, Eugene W. Stark wrote:

Sorry about the subject mess-up.  I don't know how that happened.
I changed the subject for this follow-up -- I hope I did it in a reasonable way.

I have not changed any throttling options.

The "Enter MATCH ..." messages are produced in reasonably frequent situations when
I invoke Sledgehammer by typing "try" into the main edit window.  I was aware that
they were usually throttled, but in this situation it seemed that they were not.
So maybe there is some way that the throttling gets circumvented in some situations.

That is interesting to know.

In principle, the 'try' command tries to suppress such messages, but something might be wrong in connection to sledgehammer. Maybe Jasmin wants to take a quick look himself.


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