[isabelle-dev] jEdit: Scrollbalken in Popups
Hi everyone, as can be seen on http://www21.in.tum.de/~noschinl/jedit-screenshot.png, (from Isabelle ecffea78d381 on Linux), scroll bars partially obscur the content of a popup. BTW, for theorems it would be pretty nifty, if the popup would show the theorem, not only its name. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle build glitch
On Tue, 30 Oct 2012, Lars Noschinski wrote: I deleted and reverted $ISABELLE_HOME/lib. Now everything seems to work again. As a data point: While executing the first isa build, another instance of this Isabelle instance was running. This should already be sufficient to explain it: the build process silently assumes sequentialism, like many other administrative scripts in Isabelle. I have been applying the Clint Eastwood approach to sequential things in regular Isabelle user space in the past couple of years: shooting first when they show their face, and then ask questions. For non-user-space things like online build of certain components, I don't have any such ambitions. You are supposed to take care of it yourself, like you did here already. It is just one of these difference in comfort of official releases compared to self-build repository snapshots. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Scrollbalken in Popups
On Fri, 16 Nov 2012, Lars Noschinski wrote: Hi everyone, as can be seen on http://www21.in.tum.de/~noschinl/jedit-screenshot.png, (from Isabelle ecffea78d381 on Linux), scroll bars partially obscur the content of a popup. BTW, for theorems it would be pretty nifty, if the popup would show the theorem, not only its name. See also this thread: http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03350.html It is merely a matter that I did not find time yet to figure out these two main things: (1) precise size of jEdit TextArea inner components (the Painter) (2) control of scrollbars related to that Apart from getting the window size vs TextArea painter size right, I also have the ambition to suppress scrollbars if they are not needed (i.e. in most situations). This requires a very accurate job with the metrics etc. and the scrollbars really need to be there when there are required, otherwise the user won't see parts of the text. If someone else wants to investigate the jEdit sources while I am busy elsewhere, I am keen to get some explanations how I have to approach it. Such jEdit issues typically require 2 hours, 2 days, or 2 weeks to study its sources. I guess this instance is between 2 hours and 2 days. 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] Shadowing of theorem names in locales
On Thu, 11 Oct 2012, Johannes Hölzl wrote: HOL-Probability (in Isabelle/bb5db3d1d6dd) and Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this patch. A surprising change is found in Markov_Models: We get an error when an assumption has the same name as a fact in the locale: locale loc begin lemma X: True .. lemma assumes X: X shows True ^- raises Duplicate fact declaration local.X vs. local.X Is this easily avoidable? I think this might confuse people and add a maintenance burden when one adds a fact to a locale with a popular name. It is a consequence of handling the local fact name space in a fully authentic way. In the conversions I had done earlier, there were a few situations with duplicate assumptions of a long statement, so I just renamed them apart. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] SML/NJ happiness
Isabelle/5e01e32dadbe is the result of spending some hours with SML/NJ and the ever growing HOL image. In the end it turned out as rather trivial thing: Time.+ needs to be used in this qualified manner, since the adhoc overloading of + on different ML systems works differently. I can't say on the spot why isatest gave uninformative exception Option raised here for almost two weeks, but it was relatively easy to see the point of failure in the mira reports. SML/NJ might appear like a cruel tool for torture now, but it is just a look back in time. 10 years ago, SML/NJ and Poly/ML were almost equal in performance, and SML/NJ had slightly better error messages than Poly/ML. The difference is that a lot of work has been done on Poly/ML and its integration into Isabelle (both Isar and Prover IDE), to make the comfy chair really comfortable. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
