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:

ML ‹
  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:

  PIDE.session.protocol_command("error")
  PIDE.session.protocol_command("interrupt")

The (unbuffered) result in Raw Output will be like this:

  Isabelle protocol command failure: "interrupt"
  Interrupt
  Isabelle protocol command failure: "error"
  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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.