src/Tools/jEdit/src/rendering.scala
changeset 50542 58bd88159f8f
parent 50507 9605b0d93d1e
child 50543 42bbe637be54
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:01:07 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:16:16 2012 +0100
     1.3 @@ -527,4 +527,16 @@
     1.4            if text_colors.isDefinedAt(m) => text_colors(m)
     1.5          })
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* nested text structure -- folds */
    1.10 +
    1.11 +  private val fold_depth_include = Set(Markup.SUBGOAL)
    1.12 +
    1.13 +  def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
    1.14 +    snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
    1.15 +      {
    1.16 +        case (depth, Text.Info(_, XML.Elem(Markup(name, _), _)))
    1.17 +        if fold_depth_include(name) => depth + 1
    1.18 +      })
    1.19  }