Re: [isabelle] New error messages in Isabelle 2013
On Mon, 28 Jan 2013, Gottfried Barrow wrote:
I have these commands in:
I have worked very hard to eliminate the need for these in most practical
situations. You don't need this information all the time, only when
something is wrong. Then you use CTRL-hover etc. to look what is there.
There ends up being a lot of information for a proof step, and the
output panel allows me to fix the location and size of the window for
how I prefer to view that information.
There is an option for "tooltip margin" to control the window width in a
soft manner. The location is determined by the location of the
information in the source text. This is a very important principle of the
Prover IDE, and the direction where it is moving for several years
I also get an error window popping up when I'm typing something new
because my syntax isn't right because I haven't finished it all.
This sounds more like a variation of platform-specific focus handling.
Error message popups only show up for red squiggles in the text. Maybe
you have the mouse pointer in the way, or maybe there is some Windows snag
behind it (I am more used to Linux and Mac OS X snags in that respect).
I set "Editor Chart Delay" to 10, but these windows keep occasionally
popping up. If I keep typing, it rings an error bell for each keystroke,
and the window is visually in the way.
See the option tooltip for what this is for. Tooltip timing is determined
by certain Java/Swing properties, but I don't know exactly which one.
I wouldn't put the output panel in the category of being old-style. It's
a left, right, or bottom dockable window that's part of a modern, GUI
editor. Being able to look at both the edit buffer and the output panel
at the same time at least gives it a dual focus ability.
That is old-school Proof General mode. When developing complex formal
documents you need more than dual (or triple) focus, but it does not work
by putting more windows there. One needs to make the one main window
smarter: the source window.
This archive was generated by a fusion of
Pipermail (Mailman edition) and