Re: [isabelle-dev] jedit: zoom with cmd+<+>

2013-01-08 Thread Steffen Juilf Smolka
The problem is still there on Mountain Lion with an American keyboard. However, rebinding the kebyoard shortcut locally as you suggested does the trick - thanks for the tip! Here is an ugly hack (based on the KeyEventDemo you provided) that would solve the problem: KeyEvent e_ = null; // pressi

Re: [isabelle-dev] Purpose of additional HOL images

2013-01-08 Thread Florian Haftmann
> This is a left-over from the isabelle build reform from last summer: Do > the additional HOL images still have a purpose? Notably: > > HOL-Base > HOL-Plain > HOL-Main If HOL-Plain vanished, the same could apply to Plain.thy itself. Florian -- PGP available: http://home.inform

Re: [isabelle-dev] Purpose of additional HOL images

2013-01-08 Thread Florian Haftmann
Am 07.01.2013 13:06, schrieb Makarius: > This is a left-over from the isabelle build reform from last summer: Do > the additional HOL images still have a purpose? Notably: > > HOL-Base > HOL-Plain > HOL-Main > > If it is just for experimentation, these session can be easily provided > by 1

Re: [isabelle-dev] Semantics of hide (open)

2013-01-08 Thread Florian Haftmann
>> Maybe there is some confusion what the semantics of hide (open) is >> exactly supposed to be. But since the current state of affairs gives >> no tool at hand to resolve situations as sketched above, this is a >> serious obstacle. > > The "hide" feature was added as a temporary workaround for t

Re: [isabelle-dev] Max threads & Sledgehammer

2013-01-08 Thread David Matthews
On 07/01/2013 17:49, Stefan Berghofer wrote: You could certainly hit limits on memory for stacks with a large number of threads particularly if the default stack size is large. What does "ulimit -s" say? You could try setting that smaller. "ulimit -s" says 102400 This is surprisingly large.

Re: [isabelle-dev] Proposing extensions to the Isabelle library?

2013-01-08 Thread Florian Haftmann
Hi Alessandro, > Is there any plan to make things in the library more uniform (one way or > the other)? Is there a preference for new type classes should be > developed (purely syntactic or with assumptions)? well, there is no big masterplan. Usually things evolve: somebody thinks about an exten