Re: [isabelle] New error messages in Isabelle 2013



On Mon, 28 Jan 2013, Gottfried Barrow wrote:

I have decided that this can be categorized under "floating vs. docked window preference".

This sounds more like an aspect of the dockable window manager in jEdit. It is nice for what it does, but could be improved. Unfortunetely, there are extremely few people now picking up the challenge to make real improvements there. I can understand that, because the slightest change in window behaviour causes a lot of worries on all platforms and look-and-feel themes of Java/Swing.


Here, I use the specific example of Sledgehammer and Nitpick. You have it now where we can get the output in two different places, the output panel or by hovering the mouse over the command.

But if I know I always want to see the output, and I want to see the output as the command is running, then what I want is a panel, docked or floating, that's specifically displayed for that purpose. I also want it fixed in size and location.

It is merely a technical snag that the tooltip popups are not dynamically updated, so Output is presently the only way to get incremental output on the spot as it arrives.

Looking at the bigger picture, the command + output mode of Sledgehammer and Nitpick is just a historical accident. The long-standing plan is to provide more direct support for "asynchronous agents" in the Prover IDE to produce feedback on the text as you write it. Such an agent would have its own panel somewhere to control it, although the feedback is more likely to appear around the text itsel, like a spell-checker; or as some icons or bubbles indicating suggestions to the user.


There's more info to be seen than can be displayed, so I like the jEdit plugin model. You can display or not display a window for a plugin. You can dock or not dock a window you display. You can dock a window in 4 different places. That's a lot of options on how to display information.

Note that in jEdit "plugin" is just some Java module loaded in a certain way. You probably mean "dockable window", the thing that is managed by the "dockable window manager". The Isabelle plugin provides several dockable windows: Output, Symbols, Theories etc.

4 different places for docking are nice, but I can imagine much more sophistication. Someone made an alternative dockable window manager for jEidt called "MyDoggy", but it now looks unmaintained and outdated. One could invest more here, but I am certainy not doing it myself.


Old skool with improvements, along with completely new features is sometimes the best way to go. But that's easy for me to say, and I don't have to implement it.

There is always a continous ongoing process of improvements. Keywords like "new" and "feature" are marked as dangerous in my vocabulary, though. Progress requires clear concepts first and then a long way to get it through in the implementation, and finally reach users.


	Makarius





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