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