src/Tools/jEdit/src/fold_handling.scala
Sat, 15 Dec 2012 12:16:16 +0100 wenzelm fold handling within Pretty_Text_Area, based on formal document content, which is static here;
less more (0) tip