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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and