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
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.
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 the lack of
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 line
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:
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;
//
