Re: [isabelle-dev] jedit Replace Find
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
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. Tobias Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
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? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
On Tue, 2 Oct 2012, Tobias Nipkow wrote: For example 03bc7afe8814 There is certainly not a general problem of jedit and JVM on Mac OS that covers all versions of the past and future. Funny things on Mac OS have happened before, but were sorted out at some point, by looking very closely which version of what was used of what component. Actually, what is your Mac OS version? The Mac Pro in my office runs Snow Leopard most of the time, while my MacBook is on Mountain Lion already. I am not testing Lion much. There are two sources of problems with Java/jEdit on Mac OS to be anticipated for the coming months: (1) Special cases in jEdit to accomodate former Apple Java 1.6 now work against Oracle Java 1.7. I've already removed some old key handler workaround to make normal COMMAND-C/X/V work without further ado on Java 1.7. (2) Java 1.7 is officially supported by Oracle only for Lion and Mountain Lion, but usually happens to work on Snow Leopard as well. They don't make plans against it, but they don't support it specifically. In the testing phase of Java 1.7, Oracle had a version for Snow Leopard that was based on a certain update/patch for Apple's Java 1.6. Thus my local machine might now look slightly different to official Java 1.7 and have fewer problems in that respect. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
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. Can you give your current Isabelle changeset id? Not just as a habit on the isabelle-dev mailing list, but to make any sense for such a report. There is certainly not a general problem of jedit and JVM on Mac OS that covers all versions of the past and future. Funny things on Mac OS have happened before, but were sorted out at some point, by looking very closely which version of what was used of what component. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
For example 03bc7afe8814 Tobias Am 02/10/2012 20:11, 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. Can you give your current Isabelle changeset id? Not just as a habit on the isabelle-dev mailing list, but to make any sense for such a report. There is certainly not a general problem of jedit and JVM on Mac OS that covers all versions of the past and future. Funny things on Mac OS have happened before, but were sorted out at some point, by looking very closely which version of what was used of what component. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
