[isabelle-dev] jEdit: Loading theories does not work

[Makarius]

On Fri, 13 Jan 2012, Lars Noschinski wrote:

> On 13.01.2012 13:49, Lars Noschinski wrote:
>> Hi,
>> 
>> lately, Isabelle/jEdit stopped working for me on my work laptop. The
>> Isabelle process is started (the usual startup phrase is displayed in
>> the log windows), but the status is displayed as "startup". In
>> particular, no parsing, syntax coloring or proof checking happens; the
>> polyml processes seem to be mostly idle. I bisected the problem down to
>> the following commit:
>
> Please ignore this for now; if found an error in my test setup. Will try 
> again on monday.

OK, please keep me up to date about the situation.


Last week I've only had a brief look at the change 30a69cd8a9a0 that 
you've quoted, but did not see anything suspicious and could not reproduce 
the described problem.

Generally, strange phenomena when moving between machines and/or plaforms 
occasionally did happen in the past.  For example, the startup phase and 
pipe synchronization turned out as unreliable on Windows/Cygwin, so I made 
and alternative mechanism based on sockets, see 
http://isabelle.in.tum.de/repos/isabelle/file/f23dc7d16c0b/src/Pure/System/system_channel.scala#l18, 
but this exposed some oddities with sockets in some Poly/ML versions that 
we still support officially.  I ended up tinkering almost one week on the 
seemingly trivial problem of connecting too processes by a reliable 
byte-channel.


Those who are brave enough to test the repository verions by "using" it 
regularly are welcome to post whatever oddities they observe.  This is how 
things can get ironed out eventually.


 	Makarius