Stream: Mirror: Isabelle Development Mailing List

Topic: Inconsistent behavior of indent-lines in jEdit

view this post on Zulip Email Gateway (May 31 2026 at 14:34):

From: Balazs Toth <balazs.toth@lmu.de>

If I enable the setting "Restore previously open files on startup" and
restart jEdit, then indenting lines (automatic on new line and via the
short-cut) puts everything to the start of the lines.

I can consistently reproduce it on my MacBook.

Balazs

view this post on Zulip Email Gateway (Jun 25 2026 at 10:31):

From: Balazs Toth <balazs.toth@lmu.de>

On 31.05.26 16:34, Balazs Toth wrote:

If I enable the setting "Restore previously open files on startup" and
restart jEdit, then indenting lines (automatic on new line and via the
short-cut) puts everything to the start of the lines.

I can consistently reproduce it on my MacBook.

Balazs

Hi all,

I investigated the issue and wrote a small patch.

Reproduction:

  1. In jEdit, enable "Restore previously open files on startup".
  2. With a theory file open, restart jEdit so the .thy buffer is restored.
  3. In the restored buffer, auto-indent on a new line, or invoke the
       "indent-lines" action: both move everything to column 0.

Syntax highlighting (and everything else) keeps working; only indentation
is affected. Opening a theory the normal way (after startup) is fine.

Cause:

Text_Structure.Indent_Rule is injected into jEdit's
shared Mode object by Token_Markup.Mode_Provider.loadMode. That provider is
installed in Main_Plugin.init_mode_provider(), but the main plugin is
"activate=defer", so the swap happens late.

With restore on startup, jEdit reopens the .thy buffers during
finishStartup
and loads the isabelle mode before the main plugin is activated.
Mode loading is a one-shot (Mode.loadIfNecessary guards on marker == null),
so the mode is loaded by the original ModeProvider, without the indent
rule,
and is never reloaded once the provider is installed. indent-lines then
falls
back to the mode's default rules.

Highlighting is unaffected because the token marker is set per buffer in
Buffer_Model.init_token_marker().

Patch:

After installing the PIDE Mode_Provider, re-apply the per-mode setup to
modes
that were already loaded before the swap. I factored out the setup out of
loadMode into Mode_Provider.init_mode, which I call in
init_mode_provider.

The patch (attached) applies on top of 7b3c7c9d30ce. Built with
"isabelle jedit -b" and verified: with restore on startup
enabled, indentation in restored theories now behaves as usual.

Balazs

isabelle_jedit_indent_restore.patch
OpenPGP_signature.asc

Last updated: Jul 13 2026 at 06:55 UTC