[isabelle-dev] Isabelle gets stuck when imported theory is not found

[Makarius]

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