Inconsistent behavior of indent-lines in jEdit

[Balazs Toth]

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

-------------- next part --------------
diff -r 7b3c7c9d30ce src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Mon Jun 22 13:20:25 2026 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Jun 23 20:20:40 2026 +0200
@@ -16,7 +16,7 @@
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager}
 import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.syntax.ModeProvider
+import org.gjt.sp.jedit.syntax.{ModeProvider, TokenMarker}
 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, BufferChanging, PositionChanging,
   EditPaneUpdate, PropertiesChanged, ViewUpdate}
 import org.gjt.sp.util.Log
@@ -426,8 +426,13 @@
   def init_mode_provider(): Unit = {
     orig_mode_provider = ModeProvider.instance
     if (orig_mode_provider.isInstanceOf[ModeProvider]) {
-      pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider)
-      ModeProvider.instance = pide_mode_provider
+      val provider = new Token_Markup.Mode_Provider(orig_mode_provider)
+      pide_mode_provider = provider
+      ModeProvider.instance = provider
+      for {
+        mode <- provider.getModes
+        if Untyped.get[TokenMarker](mode, "marker") != null
+      } provider.init_mode(mode)
     }
   }
 
diff -r 7b3c7c9d30ce src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Jun 22 13:20:25 2026 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jun 23 20:20:40 2026 +0200
@@ -316,11 +316,15 @@
   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider {
     for (mode <- orig_provider.getModes) addMode(mode)
 
-    override def loadMode(mode: Mode, xmh: XModeHandler): Unit = {
-      super.loadMode(mode, xmh)
+    def init_mode(mode: Mode): Unit = {
       Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker)
       Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
         Untyped.set[JList[IndentRule]](mode, "indentRules", JList.of(indent_rule)))
     }
+
+    override def loadMode(mode: Mode, xmh: XModeHandler): Unit = {
+      super.loadMode(mode, xmh)
+      init_mode(mode)
+    }
   }
 }
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260625/7f4f289a/attachment.sig>