PIDE regression in changeset 85282:4bc8b5568fd9

[Makarius]

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