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 control key.

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 MHonArc.