Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing

On Wed, 29 Oct 2014, Andreas Lochbihler wrote:

Here is another datapoint in the greyout story with Isabelle2014. The attached syslog ends with a DUP exception. This time there were no exceptions on the command line. The greyout happened again while I was using the query panel to find theorems.

The syslog ultimately says this:

  Isabelle protocol command failure: "Document.update"
  exception DUP ~5951 raised (line 261 of "General/table.ML")

which refers to Table.update_new.

Looking at the source, I did not find a plausible way how this exception could have happened -- there are normally handlers to say something more specific like ERROR "Duplicate command: ~5951".

If you see anything like this again, please tell me about it.

In Isabelle/f4e9bd04e1d5 I have reduced the chances of such low-level DUP exceptions, although that might not be directly relevant. We should continue this on isabelle-dev next time.



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