Re: [isabelle] jEdit apparantly proves False
On 11/22/2013 4:16 PM, Makarius wrote:
The history text field updates its history when you type RETURN into
it, which then also has the effect of "Apply". The Apply button alone
does not update the history.
That does it. In the find panel and sledgehammer panel, I was executing
the commands with the mouse.
I make a tangent here, which is not a complaint. It's just to inform you
on how some people work, and how it's related to getting info in the IDE.
I work a lot with my right hand on the mouse, and my left hand far away
from the keyboad. That causes me to prefer looking at info in the output
panel, rather than moving my left hand to the keyboard to press the
There are also two other things which prevent me from taking full
advantage of the info you make available. In the IDE gutter, I always
have line numbers displayed. Consequently, your icons aren't displayed.
As far as I can tell, I can't show both line numbers and information
icons in the gutter.
I also set the tooltip delay to about 1.5 seconds, because in Windows,
when I start typing, I immediately get an error, and a popup window pops
up where the mouse cursor is, which is where the text cursor is, and it
beeps at me for every character I type. The workaround is to move the
mouse cursor away from the text cursor before I begin typing, but I
don't remember to do that, so I set the tooptip delay to be long, which
is not optimal for cntl-mouse hovering.
You don't need to respond to any of that. I say it to explain that there
are a number of reasons that keep me hooked on output panel for info,
among which is wanting to see lots of info at once, primarily to see all
of the typing, bracketing, and constants.
Note that for Isabelle2013-2, I did already change the spontaneous
restart behaviour of sledgehammer after editing the text:
You can try that when Isabelle2013-2-RC1 appears.
Okay. I'll try it out. I never actually switched beyond
Isabelle2013-1-RC3, except for a small test of Isabelle2013-1 on my laptop.
This archive was generated by a fusion of
Pipermail (Mailman edition) and