On Mon, 16 Mar 2015, Makarius wrote:
I have reworked this substantially in various changesets leading up to
5d0c539537c9. It is surprising how much time can be spent on such details.
Now there is even some semantic completion, to propose a theory name that
fits to the file name, in the error saying that there is a disagreement.
A note to enthusiastioc testers: in the above version the 'theory' keyword
needs to be right at the start of the file. It is presently a consequence
of slightly odd mismatches of command spans vs. formal headers.
This is only a small gimmick. The IDE could have in principle much more
"do it for me" features, but that is a lot of work to implement and
maintain.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
