[isabelle-dev] jedit Replace & Find

Makarius makarius at sketis.net
Mon Nov 19 17:10:17 CET 2012


On Sun, 18 Nov 2012, Tobias Nipkow wrote:

> Am 16/11/2012 14:47, schrieb Makarius:
>> On Tue, 2 Oct 2012, Tobias Nipkow wrote:
>>
>>> This is what you should not do: search and replace a string 
>>> selectively that occurs many times in a theory. I did this twice (the 
>>> second time to see if it was repeatable), using Replace & Find, and 
>>> after about 50 replacements, jedit went all funny and screwed up the 
>>> window manager on my mac. Once I managed to log out (and back in), the 
>>> window manager was fine again.
>>
>> Did you ever see this incident with Mac OS X again?
>
> Yes, I just retried and the beahviour is unchanged (it may have take a 
> bit longer to provoke it). Open Wellfounded.thy and replace wf by 
> something, that does it.

This way I managed to reproduce the problem after some rounds of clicking, 
using Snow Leopard both with the native "Mac OS X" and "Nimbus" look & 
feel. Mountain Lion appears to work, at least I did not see anything bad 
after trying the same 4-5 times longer than on Snow Leopard.

So it might be just bad luck of Java 7 on Snow Leopard.  Oracle says it 
does nothing against it nor for it.  So if Java 7 happens to work on what 
Apple considers legacy already, it is mere luck.


 	Makarius




More information about the isabelle-dev mailing list