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

Last updated: Jun 04 2026 at 18:19 UTC