changeset 50545 | 00bdc48c5f71 |
parent 50543 | 42bbe637be54 |
child 50547 | ebd75dfaab73 |
--- a/src/Tools/jEdit/src/rendering.scala Sat Dec 15 12:54:14 2012 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Sat Dec 15 12:55:11 2012 +0100 @@ -531,7 +531,7 @@ /* nested text structure -- folds */ - private val fold_depth_include = Set(Markup.GOAL, Markup.SUBGOAL) + private val fold_depth_include = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL) def fold_depth(range: Text.Range): Stream[Text.Info[Int]] = snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>