src/Tools/jEdit/src/rendering.scala

--- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:01:07 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:16:16 2012 +0100
@@ -527,4 +527,16 @@
           if text_colors.isDefinedAt(m) => text_colors(m)
         })
   }
+
+
+  /* nested text structure -- folds */
+
+  private val fold_depth_include = Set(Markup.SUBGOAL)
+
+  def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
+    snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
+      {
+        case (depth, Text.Info(_, XML.Elem(Markup(name, _), _)))
+        if fold_depth_include(name) => depth + 1
+      })
 }