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:

 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.


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

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

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