Auto-insert error in current development version

[Makarius]

On 05/03/2026 19:49, Lawrence Paulson via isabelle-dev wrote:
> In recent versions e.g. 592248e8358d+ the “self-insert” feature of sledgehammer, induction proofs, etc., has stopped working.

Thanks for the hint. See now:

changeset:   84180:4b07fc817274user:        wenzelm
date:        Thu Mar 05 21:13:23 2026 +0100
files:       src/Tools/jEdit/src/rich_text_area.scala
description:
proper editor context from background view with its current TextArea, not this 
Rich_Text_Area / Popup (amending fa6b16ff71d2);


	Makarius