[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Tue, 29 Apr 2014, Matthew Fernandez wrote:

> Currently most of my theories are generated by another tool. When 
> debugging the generated theories, I often have to open a file that I 
> know contains many broken proofs. In these circumstances it can be 
> beneficial to have a way of stepping into the middle of a broken proof 
> to explore, while ignoring all the following (also broken) proofs).

In Isabelle/578dc6b4be89 and d11d11da0d90 from about 2 weeks ago there is 
a slightly refined treatment of error recovery, such that continuous 
checking no longer bumps into other toplevel statements / proofs.

That is still not the real thing, just the second round of adhoc 
improvements after the first one in 2010.  Proper structural recovery 
needs to come at some point, with more formal indendation, and the final 
discontinuation of hard tabulators -- not for the coming release, though.


 	Makarius