Re: [isabelle] New error messages in Isabelle 2013

On 1/30/2013 7:18 AM, Makarius wrote:
It works better if you disable show_types and show_sorts by default. Isabelle2013 will then add the annotations to *all* possible positions as markup to the output, and you can hover over it to see what is there and what is wrong. If show_types / show_sorts are enabled, you get the old behaviour of partial printing directly in the text.

The ambition in Isabelle2013 was to eliminate then need for show_types / show_sorts altogether -- I've got too many complaints about such options missing in the "menu". Lets see how far it is now from 0.00001 relevance.


I put in "declare[[show_types=false]] declare[[show_sorts=false]]", and I didn't see anything extra, but I'll experiment with changing "show_types" back and forth and see what happens.

As far as features and ways of doing things, after I get worked up, I then remind myself that the ideas for all of this started many years ago, and it's not the result of ideas I have about it today. I then stop worrying/caring, and start trying to get some work done with however it works. Speaking of "many years ago", I also keep in mind the "engine work" that started over 40 years ago.

However, I make one last point, for the time being.

Trying to go with the new flow, I start CNTRL+hovering. However, this brings up the final point: the human brain can process a massive amount of information very fast sometimes.

So when I start hovering over the formula of a theorem, I get information about, I'd say, ten times slower than what I can process the information, and I don't think I'm exaggerating, and I don't think I'm outside the norm.

I have a formula that's four lines long, and it has about 15 items per line in it that can be hovered over. I start from left to right on a line, and I drag my mouse over the items, but nothing happens other than they turn grey, because the tooltip doesn't respond fast enough.

Well, if I'm going to drag my mouse over 45 items, then if I was writing the software, I would give myself the ability to hover over one item and get a massive amount of information about all of those 45 items, where many of those items are duplicates, though seeing what is a a duplication is not actually always quickly apparent.

I'm not writing the software, so, today, I care more about trying to use the software as it is to get something done.


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