[isabelle-dev] Isabelle gets stuck when imported theory is not found
makarius at sketis.net
Mon Mar 16 17:11:52 CET 2015
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
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.
More information about the isabelle-dev