[isabelle-dev] Bad theory import "Main"

Makarius makarius at sketis.net
Sat Apr 22 19:17:28 CEST 2017


On 22/04/17 18:10, Blanchette, J.C. wrote:
> 
> It doesn't help:
> 
> $ isabelle jedit -bf
> ### Building Isabelle/Scala ...
> ### Building Isabelle/jEdit ...
> 
> $ isabelle scala
> Welcome to Scala 2.11.8 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_121).
> Type in expressions for evaluation. Or try :help.
> 
> 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.


	Makarius





More information about the isabelle-dev mailing list