Re: [isabelle] New error messages in Isabelle 2013

On 2/1/2013 6:18 AM, Makarius wrote:
This means you can explore that recursively by hovering over formal input and output -- this is now mostly uniform in Isabelle2013. This unfolds a massive tree of information, or rather a large forest, by walking a few steps into some of its paths.

Thanks for the explanation. And we all know how much we love hyperlinks. This is definitely a "friendly IDE" feature you've added. It's good when information comes to me via hyperlinks, rather than me having to go to the information.

In case others might not have noticed yet, the hyperlinks are grey boxes with a line around them, rather than just grey boxes.

But the way it works is that some people don't forgo the old for the new, they keep the old and use the new also. But it may be the economics of IDEs, that the old has to be sacrificed for the new. And that's why there's a thriving software utility market. Microsoft gets rid of the taskbar and start button in Windows 8, and someone produces a utility to put it all back.

Of course, there are endless possibilities to refine this further. An obvious question is: What is a succinct "digest" (as output text) to give you a types / sorts environment for some formal output. Old show_types / show_sorts are traditionally very crude here. This is only a starting point for further reworking of these ancient mechanisms. In particular, I hope to see certain improvements done for current sledgehammer isar_proofs output to be taken into account as well.

Sounds like a lot of work.


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