Re: [isabelle] Message output in Isabelle2014 and Isabelle2015

On Tue, 23 Jun 2015, Peter Lammich wrote:

The deeper problem is cluttering of Output with too many different things, and the lack of a dedicated panel just for proof state output.
For those people with large screens, this may be a good solution. It already worked nicely for PG, where I usually used the "3-pane" mode, or had three windows: Text, Goal-state, Errors/Warnings.

To make up for a nice layout, I would like to dock one panel to right-top, and the other to right-bottom. Does jedit support such docking positions, that go beyond left,right,top,bottom?

We've had this topic occasionally on the mailing list. The default dockable window manager of jEdit can't do that, but it is a general "framework", so plugins can implement their own policies. Anybody interested in some Java/AWT/Swing window management should subscribe to the jedit-devel mailing list and start a discussion there.

So far I've done myself only very minimalistic tuning of the built-in window manager, e.g. to add the "Detach" menu item.

If you work on a small screen (laptop), you probably still want to have a mode that consumes less space, and sensibly mixes the outputs. However, I do not know how a PIDE-like asynchronous IDE can guess what the user currently wants to see. Perhaps, you could try a heuristics on the type of error, something like: Syntax-errors are displayed after the goal-state, failed method errors before the goal-state.

In ancient times when Proof General was alive and young (10-15 years ago), people had rather large displays and power-users even a second display just for goal state output.

Today people expect to be able to do big things with tiny mobile devices. With a really high resolution display (4K, 5K, Retina) it might actually work, if the font size is set to traditional 12px.


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