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

[Makarius]

On Thu, 5 Mar 2015, Christian Sternagel wrote:

> Just for the record. I think I experienced something similar:
>
>
> https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-January/005864.html

Thanks for the reminder.  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.


 	Makarius