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

[Makarius]

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.

This is only a small gimmick.  The IDE could have in principle much more 
"do it for me" features, but that is a lot of work to implement and 
maintain.


 	Makarius