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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
