On Thu, 5 Mar 2015, Makarius wrote:
I will try to pick up this old thread soon for the coming release. The
problem is a consequence of various "improvements" done elsewhere. I did
not make any attempt to change that yet, since I have already a better
idea to handle the files that are referenced in theory sources, both
imports and ML_files.
Thus we have a chance for a genuine improvement of that aspect in the
coming release. As we are moving towards it in Apr/May 2015, it will
need extra sharp eyes watching out for such fine points.
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
