equal
deleted
inserted
replaced
529 } |
529 } |
530 |
530 |
531 |
531 |
532 /* nested text structure -- folds */ |
532 /* nested text structure -- folds */ |
533 |
533 |
534 private val fold_depth_include = Set(Markup.SUBGOAL) |
534 private val fold_depth_include = Set(Markup.GOAL, Markup.SUBGOAL) |
535 |
535 |
536 def fold_depth(range: Text.Range): Stream[Text.Info[Int]] = |
536 def fold_depth(range: Text.Range): Stream[Text.Info[Int]] = |
537 snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ => |
537 snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ => |
538 { |
538 { |
539 case (depth, Text.Info(_, XML.Elem(Markup(name, _), _))) |
539 case (depth, Text.Info(_, XML.Elem(Markup(name, _), _))) |