Re: [isabelle] New error messages in Isabelle 2013



On Mon, 28 Jan 2013, Gottfried Barrow wrote:

I have these commands in:

 declare[[show_brackets=true]]  declare[[show_types=true]]
 declare[[names_unique=true]]   declare[[show_consts=true]]

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


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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.