Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
On Wed, 13 Aug 2014, Makarius wrote:
If Prover.echo still works after the greyout, the protocol thread is
alive and not dead-locked. The abrupt end of the syslog after
Document.update could also mean that it just crashed, but then we need
to see ML exceptions on Raw Output. The latter is unbuffered, though.
Did you have Raw Output open *before* the incident?
Just to make sure here is an example for protocol commands that crash:
Isabelle_Process.protocol_command "error" (fn _ => error "Error");
Isabelle_Process.protocol_command "interrupt" (fn _ => Exn.interrupt ());
Now the Scala console within Isabelle/jEdit can invoke them like this:
The (unbuffered) result in Raw Output will be like this:
Isabelle protocol command failure: "interrupt"
Isabelle protocol command failure: "error"
So if the Raw Output panel is active in this mysterious PIDE greyout, and
the ML protocol command loop failing, it should be visible there.
One reason for Document.update crashing could be a resource problem, which
leads to implicit interrupt in Poly/ML. Above we see that this is printed
explicitly, unlike in the normal user space error output, since this is
the PIDE machine room.
This archive was generated by a fusion of
Pipermail (Mailman edition) and