[isabelle-dev] Bad theory import "Main"

[Jasmin Blanchette]

Hello,

Something strange is happening with the repository (as per Isabelle/701bb74c5f97). This morning, I launched Isabelle on some theories in the AFP or in "src/HOL/Library". At first, I saw that Isabelle was reloading all Main theories starting with "Code_Generation" and "HOL", even though the logic was "Default (Main)". I immediately quit, and now the behavior is even worse. On the line where "Main" is imported, I get the error

	Bad theory import "Main"

Steps to reproduce the problem:

	cd src/HOL/Library
	isabelle jedit Cancellation.thy

(with or without "-l HOL"). I've attached a screenshot.

Removing the "~/.isabelle/jedit" doesn't help.

Any idea of what is going on?

Jasmin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170422/f615d4da/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bad_thy_Main.png
Type: image/png
Size: 277503 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170422/f615d4da/attachment-0001.png>