Re: [isabelle] New error messages in Isabelle 2013

On Mon, 28 Jan 2013, Gottfried Barrow wrote:

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.

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.

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.


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