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