Stream: Mirror: Isabelle Development Mailing List

Topic: Auto-insert error in current development version

view this post on Zulip Email Gateway (Mar 05 2026 at 18:49):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

In recent versions e.g. 592248e8358d+ the “self-insert” feature of sledgehammer, induction proofs, etc., has stopped working.

Larry

view this post on Zulip Email Gateway (Mar 05 2026 at 21:07):

From: Makarius <makarius@sketis.net>

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

Last updated: Mar 17 2026 at 17:04 UTC