PIDE regression in changeset 85282:4bc8b5568fd9

Manuel Eberl manuel at pruvisto.org
Fri Sep 4 20:16:11 CEST 2026


Hello,

I believe I have found an annoying regression involving PIDE and I 
successfully bisected it. The changeset in which the problem first 
occurs is:

     changeset 85282:4bc8b5568fd9, more direct use of Resources.thy for 
PIDE;

The last good changeset is the one before that:

     changeset 85281:bea102160b8b, tuned;

The problem is that when one has a theory file with a malformed header 
in Isabelle/jEdit, PIDE seems to crash and never recover and everything 
just becomes unresponsive.

Steps to reproduce:
1. Open Isabelle/jEdit
2. Create a new file and save it as "Test.thy"
3. Start typing, e.g. type in "theory"
4. Before the regression, the IDE would immediately respond saying 
something like "Theory name expected but end of line found". Now, with 
the regression, the IDE does not respond at all and syslog says 
'Isabelle protocol command failure: "Document.update"'. It does not 
recover even if you close "Test.thy" and open another, well-formed 
theory file.

Hope that helps to track down the issue.

Manuel



More information about the isabelle-dev mailing list