On Mon, 16 Mar 2015, Makarius wrote:
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.
I have reworked this in 5c1a0069b9d3 and c443ca40ef8d, so that the
'theory' keyword may be anywhere. Moreover the header format to determine
the session graph dependencies and local syntax of each editor buffer is a
bit more liberal.
It remains to be seen in the coming weeks before the Isabelle2015 release
if further details need to become more smooth. As usual, it is not
immediately clear, how the system should react on partial or broken input
during the continous editing process.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
