Stream: Mirror: Isabelle Development Mailing List

Topic: PIDE regression in changeset 85282:4bc8b5568fd9

Email Gateway (Sep 04 2026 at 18:16):

From: Manuel Eberl <manuel@pruvisto.org>

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

Email Gateway (Sep 04 2026 at 22:42):

From: Makarius <makarius@sketis.net>

On 04/09/2026 20:16, Manuel Eberl wrote:

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;

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.
Thanks for the hint, this is indeed very bad: it is a hard crash of the PIDE
protocol in the encode/decode phase of its protocol commands.

The changeset 4bc8b5568fd9 does not tell any reasons for the problem,
especially why it emerges now and not before. I will investigate this later
today (in the morning).

For now the subsequent changeset should be sufficient:

changeset: 85353:a29e6a740b79
tag: tip
user: wenzelm
date: Sat Sep 05 00:39:03 2026 +0200
summary: more robust decode_thy: messages may contain further markup, so
XML.Decode.string alone will fail;

Makarius

Last updated: Sep 15 2026 at 09:19 UTC