src/Tools/jEdit/src/text_structure.scala
changeset 73344 f5c147654661
parent 73340 0ffcad1f6130
child 73345 8204f7b53007
equal deleted inserted replaced
73343:d0378baf7d06 73344:f5c147654661
   219       close: Token => Boolean,
   219       close: Token => Boolean,
   220       reset: Token => Boolean,
   220       reset: Token => Boolean,
   221       restrict: Token => Boolean,
   221       restrict: Token => Boolean,
   222       it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
   222       it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
   223     {
   223     {
   224       val range1 = it.next.range
   224       val range1 = it.next().range
   225       it.takeWhile(info => !info.info.is_command || restrict(info.info)).
   225       it.takeWhile(info => !info.info.is_command || restrict(info.info)).
   226         scanLeft((range1, 1))(
   226         scanLeft((range1, 1))(
   227           { case ((r, d), Text.Info(range, tok)) =>
   227           { case ((r, d), Text.Info(range, tok)) =>
   228               if (open(tok)) (range, d + 1)
   228               if (open(tok)) (range, d + 1)
   229               else if (close(tok)) (range, d - 1)
   229               else if (close(tok)) (range, d - 1)