[isabelle] Feature Request: Auto Scroll in jEdit



Hi,

one thing I would love to see in jEdit is an auto scroll feature for the output panel.
There could be another checkbox next to the auto update one for quick toggling.

For example, this would make working with Sledgehammer, which produces output incrementally, much more convenient.

Aside from autoscroll, it would already be helpful if the output panel would not scroll all the way up whenever a new line of output is added but stay at the current position instead.

Best Regards
Steffen



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.