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