Re: [isabelle] New error messages in Isabelle 2013



On 1/28/2013 10:19 AM, Alfio Martini wrote:
I have sent this already in a message previous to this one. The question is
simple:
I (as many other Isabelle users, I suppose) depend very much on the output
window to work with
Isabelle even though I work essentially with Isar structured proofs. The
hover-over-the-scribbles
feature is nice, but the output window is better and faster.

I would hate to see the output panel ever go away for proof goals. If anything, I'd like to see information generated there when I click on a line for something like "definition", "consts", "notation", "abbreviation", and get any useful information that the prover engine is using that gets hidden. I have these commands in:

  declare[[show_brackets=true]]  declare[[show_types=true]]
  declare[[names_unique=true]]   declare[[show_consts=true]]

There ends up being a lot of information for a proof step, and the output panel allows me to fix the location and size of the window for how I prefer to view that information.

I also get an error window popping up when I'm typing something new because my syntax isn't right because I haven't finished it all.

I set "Editor Chart Delay" to 10, but these windows keep occasionally popping up. If I keep typing, it rings an error bell for each keystroke, and the window is visually in the way.

There's a lot of visual information that automatically gets generated, like an error icon in the gutter on the right, or the vertical bar going purple on the left, and the squiggly lines of different colors, and all that is good.

However, I would say that windows popping up to notify me of something on a frequent basis is overall a bad thing. I say more below.

Makarius wrote:

The screenshot does not show the position of the cursor (or "caret" in
Java terminology).  Where is it actually?  The output window follows that,
in reminiscence of old-style TTY interaction where you have a single focus.

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.

It comes down to personal preference, but I put a lot of effort into getting my windows all set up. With jEdit, I use a three panel view: edit buffer, left panel, and bottom panel.

It all looks nice. The popup windows are sort of ugly.

And when a window pops up I wasn't expecting that tries to help me out, when I don't want any help, because I don't care about the error, I don't really like that, and I make sure I keep a proper perspective on how powerful the Isabelle software is.

If I hover over something to intentionally get the popup window, I like that, especially when it gives me useful information.

The popup windows are a good addition, but I also like to control where my main "information" windows are, which, with jEdit, is docking them in a fixed location I want them to be.

Regards,
GB






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