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