[isabelle-dev] Bad theory import "Main"

[Makarius]

On 23/04/17 13:43, Blanchette, J.C. wrote:
>>> 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
> 
> I just pulled and updated (f533820e7248) before carrying out any further tests. Now I get the same error as Jenkins:
> 
> $ isabelle build -b HOL
> *** No such file: "/Users/blanchette/isabelle/src/HOL/Main.thy"
> *** The error(s) above occurred for theory "Main" (line 8 of "/Users/blanchette/isabelle/src/HOL/ROOT")
> *** The error(s) above occurred in session "HOL" (line 3 of "/Users/blanchette/isabelle/src/HOL/ROOT")

That is unrelated. I merely made the most basic mistake in Mercurial
usage, see now:

changeset:   65553:006a274cdbc2
user:        wenzelm
date:        Sun Apr 23 14:15:09 2017 +0200
files:       src/HOL/Main.thy
description:
added missing file (amending f533820e7248);


Concerning the actual problem, I have now made the session_base error
strict (again):

changeset:   65554:a04afc400156
tag:         tip
user:        wenzelm
date:        Sun Apr 23 14:27:22 2017 +0200
files:       src/Tools/jEdit/src/plugin.scala
description:
prefer strict operation (despite 8edca3465758): there might be errors
from all_known = true (ae09b9f5980b);


This means you should see some "Java vomit" on the terminal at startup
of Isabelle/jEdit, as well as some text popup with a half-decent error
message. Plugin startup is always a bit fragile.


	Makarius