more elementary list structures for markup tree traversal;
authorwenzelm
Wed Aug 07 19:59:58 2013 +0200 (2013-08-07 ago)
changeset 52900d29bf6db8a2d
parent 52899 3ff23987f316
child 52901 8be75f53db82
more elementary list structures for markup tree traversal;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/fold_handling.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 07 17:23:40 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 07 19:59:58 2013 +0200
     1.3 @@ -328,11 +328,11 @@
     1.4        range: Text.Range,
     1.5        info: A,
     1.6        elements: Option[Set[String]],
     1.7 -      result: Command.State => (A, Text.Markup) => Option[A]): Stream[Text.Info[A]]
     1.8 +      result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
     1.9      def select_markup[A](
    1.10        range: Text.Range,
    1.11        elements: Option[Set[String]],
    1.12 -      result: Command.State => Text.Markup => Option[A]): Stream[Text.Info[A]]
    1.13 +      result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
    1.14    }
    1.15  
    1.16    type Assign_Update =
    1.17 @@ -564,21 +564,22 @@
    1.18              })
    1.19  
    1.20          def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
    1.21 -          result: Command.State => (A, Text.Markup) => Option[A]): Stream[Text.Info[A]] =
    1.22 +          result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    1.23          {
    1.24            val former_range = revert(range)
    1.25 -          for {
    1.26 -            (command, command_start) <- node.command_range(former_range).toStream
    1.27 +          (for {
    1.28 +            (command, command_start) <- node.command_range(former_range)
    1.29              st = state.command_state(version, command)
    1.30              res = result(st)
    1.31              Text.Info(r0, a) <- st.markup.cumulate[A](
    1.32                (former_range - command_start).restrict(command.range), info, elements,
    1.33 -              { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) })
    1.34 -          } yield Text.Info(convert(r0 + command_start), a)
    1.35 +              { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
    1.36 +            ).iterator
    1.37 +          } yield Text.Info(convert(r0 + command_start), a)).toList
    1.38          }
    1.39  
    1.40          def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.41 -          result: Command.State => Text.Markup => Option[A]): Stream[Text.Info[A]] =
    1.42 +          result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
    1.43          {
    1.44            def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
    1.45            {
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 17:23:40 2013 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 19:59:58 2013 +0200
     2.3 @@ -223,7 +223,7 @@
     2.4      to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
     2.5  
     2.6    def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
     2.7 -    result: (A, Text.Markup) => Option[A]): Stream[Text.Info[A]] =
     2.8 +    result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
     2.9    {
    2.10      val notable: Elements => Boolean =
    2.11        result_elements match {
    2.12 @@ -242,42 +242,42 @@
    2.13        if (changed) Some(y) else None
    2.14      }
    2.15  
    2.16 -    def stream(
    2.17 +    def traverse(
    2.18        last: Text.Offset,
    2.19 -      stack: List[(Text.Info[A], Stream[(Text.Range, Entry)])]): Stream[Text.Info[A]] =
    2.20 +      stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] =
    2.21      {
    2.22        stack match {
    2.23 -        case (parent, (range, entry) #:: more) :: rest =>
    2.24 +        case (parent, (range, entry) :: more) :: rest =>
    2.25            val subrange = range.restrict(root_range)
    2.26            val subtree =
    2.27              if (notable(entry.subtree_elements))
    2.28 -              entry.subtree.overlapping(subrange).toStream
    2.29 -            else Stream.empty
    2.30 +              entry.subtree.overlapping(subrange).toList
    2.31 +            else Nil
    2.32            val start = subrange.start
    2.33  
    2.34            (if (notable(entry.elements)) results(parent.info, entry) else None) match {
    2.35              case Some(res) =>
    2.36                val next = Text.Info(subrange, res)
    2.37 -              val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
    2.38 -              if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
    2.39 +              val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
    2.40 +              if (last < start) parent.restrict(Text.Range(last, start)) :: nexts
    2.41                else nexts
    2.42 -            case None => stream(last, (parent, subtree #::: more) :: rest)
    2.43 +            case None => traverse(last, (parent, subtree ::: more) :: rest)
    2.44            }
    2.45  
    2.46 -        case (parent, Stream.Empty) :: rest =>
    2.47 +        case (parent, Nil) :: rest =>
    2.48            val stop = parent.range.stop
    2.49 -          val nexts = stream(stop, rest)
    2.50 -          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
    2.51 +          val nexts = traverse(stop, rest)
    2.52 +          if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts
    2.53            else nexts
    2.54  
    2.55          case Nil =>
    2.56            val stop = root_range.stop
    2.57 -          if (last < stop) Stream(Text.Info(Text.Range(last, stop), root_info))
    2.58 -          else Stream.empty
    2.59 +          if (last < stop) List(Text.Info(Text.Range(last, stop), root_info))
    2.60 +          else Nil
    2.61        }
    2.62      }
    2.63 -    stream(root_range.start,
    2.64 -      List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
    2.65 +    traverse(root_range.start,
    2.66 +      List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
    2.67    }
    2.68  }
    2.69  
     3.1 --- a/src/Tools/jEdit/src/fold_handling.scala	Wed Aug 07 17:23:40 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/fold_handling.scala	Wed Aug 07 19:59:58 2013 +0200
     3.3 @@ -31,7 +31,7 @@
     3.4          if (i < 0) 0
     3.5          else {
     3.6            rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match {
     3.7 -            case d #:: _ => d
     3.8 +            case d :: _ => d
     3.9              case _ => 0
    3.10            }
    3.11          }
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 17:23:40 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 19:59:58 2013 +0200
     4.3 @@ -193,7 +193,7 @@
     4.4              if (highlight_include(elem.name))
     4.5                Some(Text.Info(snapshot.convert(info_range), highlight_color))
     4.6              else None
     4.7 -        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
     4.8 +        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
     4.9    }
    4.10  
    4.11  
    4.12 @@ -244,7 +244,7 @@
    4.13              }
    4.14  
    4.15            case _ => None
    4.16 -        }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
    4.17 +        }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None }
    4.18    }
    4.19  
    4.20  
    4.21 @@ -263,7 +263,7 @@
    4.22                  elem.name == Markup.SENDBACK)
    4.23                Some(Text.Info(snapshot.convert(info_range), elem))
    4.24              else None
    4.25 -        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    4.26 +        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    4.27  
    4.28  
    4.29    def command_results(range: Text.Range): Command.Results =
    4.30 @@ -293,7 +293,7 @@
    4.31              Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
    4.32  
    4.33            case _ => None
    4.34 -        }).toList.flatMap(_.info)
    4.35 +        }).flatMap(_.info)
    4.36      if (results.isEmpty) None
    4.37      else {
    4.38        val r = Text.Range(results.head.range.start, results.last.range.stop)
    4.39 @@ -366,7 +366,7 @@
    4.40              if (tooltips.isDefinedAt(name))
    4.41                Some(add(prev, r, (true, XML.Text(tooltips(name)))))
    4.42              else None
    4.43 -        }).toList.map(_.info)
    4.44 +        }).map(_.info)
    4.45  
    4.46      results.map(_.info).flatMap(_._2) match {
    4.47        case Nil => None
    4.48 @@ -424,7 +424,7 @@
    4.49  
    4.50    private val squiggly_include = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    4.51  
    4.52 -  def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
    4.53 +  def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
    4.54    {
    4.55      val results =
    4.56        snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ =>
    4.57 @@ -482,9 +482,7 @@
    4.58  
    4.59  
    4.60    def output_messages(st: Command.State): List[XML.Tree] =
    4.61 -  {
    4.62      st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
    4.63 -  }
    4.64  
    4.65  
    4.66    private val background1_include =
    4.67 @@ -492,9 +490,9 @@
    4.68        Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
    4.69        active_include
    4.70  
    4.71 -  def background1(range: Text.Range): Stream[Text.Info[Color]] =
    4.72 +  def background1(range: Text.Range): List[Text.Info[Color]] =
    4.73    {
    4.74 -    if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
    4.75 +    if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
    4.76      else
    4.77        for {
    4.78          Text.Info(r, result) <-
    4.79 @@ -531,7 +529,7 @@
    4.80    }
    4.81  
    4.82  
    4.83 -  def background2(range: Text.Range): Stream[Text.Info[Color]] =
    4.84 +  def background2(range: Text.Range): List[Text.Info[Color]] =
    4.85      snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
    4.86        {
    4.87          case Text.Info(_, elem) =>
    4.88 @@ -539,7 +537,7 @@
    4.89        })
    4.90  
    4.91  
    4.92 -  def bullet(range: Text.Range): Stream[Text.Info[Color]] =
    4.93 +  def bullet(range: Text.Range): List[Text.Info[Color]] =
    4.94      snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
    4.95        {
    4.96          case Text.Info(_, elem) =>
    4.97 @@ -550,7 +548,7 @@
    4.98    private val foreground_include =
    4.99      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ)
   4.100  
   4.101 -  def foreground(range: Text.Range): Stream[Text.Info[Color]] =
   4.102 +  def foreground(range: Text.Range): List[Text.Info[Color]] =
   4.103      snapshot.select_markup(range, Some(foreground_include), _ =>
   4.104        {
   4.105          case Text.Info(_, elem) =>
   4.106 @@ -586,10 +584,9 @@
   4.107  
   4.108    private val text_color_elements = text_colors.keySet
   4.109  
   4.110 -  def text_color(range: Text.Range, color: Color)
   4.111 -      : Stream[Text.Info[Color]] =
   4.112 +  def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   4.113    {
   4.114 -    if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
   4.115 +    if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
   4.116      else
   4.117        snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
   4.118          {
   4.119 @@ -602,7 +599,7 @@
   4.120  
   4.121    private val fold_depth_include = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   4.122  
   4.123 -  def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
   4.124 +  def fold_depth(range: Text.Range): List[Text.Info[Int]] =
   4.125      snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
   4.126        {
   4.127          case (depth, Text.Info(_, elem)) =>