Re: [isabelle] New error messages in Isabelle 2013
On 1/28/2013 12:56 PM, Makarius wrote:
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.
But that is your personal preference, which reigns supreme in
influencing your decisions on what features to add or eliminate.
Myself, I greatly appreciate that Isar syntax allows many implicit
meanings, but I currently always want to see explicit typing and
grouping used for the constants and the formulas for a proof step. It's
a happy medium. I don't have to clutter up the code, but I always get to
check the typing and grouping without having to do anything other than
look down at the output panel.
Do do that now, if the output panel is docked at the bottom, I merely
have to shift my eyes down to the bottom of the editor.
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
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.
I have decided that this can be categorized under "floating vs. docked
Suppose the need was eliminated to display any of the proof step
information in the output panel. I forsee in the future that someone
would make a request like this: "Makarius, you know those different
kinds of popup windows that give us information? Can you make it where
we can choose for them to be either floating or dockable? You might have
an options button which allows us to select or deselect error info,
proof info, term info, etc. "
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.
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and