[isabelle-dev] Bad theory import "Main"

[Makarius]

On 22/04/17 19:34, Blanchette, J.C. wrote:
> 
>> On 22.04.2017, at 19:17, Makarius <makarius at sketis.net> wrote:
>>
>>> scala> PIDE.resources.session_base.known.files.toList.find(p => p._2.exists(_.theory == "Main"))
>>> <console>:12: error: not found: value PIDE
>>>       PIDE.resources.session_base.known.files.toList.find(p => p._2.exists(_.theory == "Main"))
>>>       ^
>>
>> You need to do this in the Console plugin of Isabelle/jEdit, switched
>> into Scala mode.
> 
> I see. It prints
> 
> 	res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] = None

There is probably something wrong with the general session layout.  The
critical changeset shows an old fallback to Pure:
http://isabelle.in.tum.de/repos/isabelle/rev/ae09b9f5980b#l4.10

You should see the error like this in the Console/Scala plugin:

val dirs = JEdit_Sessions.session_dirs()
val session_base = Sessions.session_base(PIDE.options.value, "HOL", dirs
= dirs, all_known = true)


	Makarius