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

[Makarius]

On Mon, 16 Mar 2015, Makarius wrote:

> 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.

I have reworked this in 5c1a0069b9d3 and c443ca40ef8d, so that the 
'theory' keyword may be anywhere.  Moreover the header format to determine 
the session graph dependencies and local syntax of each editor buffer is a 
bit more liberal.

It remains to be seen in the coming weeks before the Isabelle2015 release 
if further details need to become more smooth.  As usual, it is not 
immediately clear, how the system should react on partial or broken input 
during the continous editing process.


 	Makarius