src/Tools/jEdit/src/rendering.scala
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), _ =>