more elementary list structures for markup tree traversal;

--- a/src/Pure/PIDE/document.scala	Wed Aug 07 17:23:40 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 07 19:59:58 2013 +0200
@@ -328,11 +328,11 @@
       range: Text.Range,
       info: A,
       elements: Option[Set[String]],
-      result: Command.State => (A, Text.Markup) => Option[A]): Stream[Text.Info[A]]
+      result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
     def select_markup[A](
       range: Text.Range,
       elements: Option[Set[String]],
-      result: Command.State => Text.Markup => Option[A]): Stream[Text.Info[A]]
+      result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
   }
 
   type Assign_Update =
@@ -564,21 +564,22 @@
             })
 
         def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
-          result: Command.State => (A, Text.Markup) => Option[A]): Stream[Text.Info[A]] =
+          result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
         {
           val former_range = revert(range)
-          for {
-            (command, command_start) <- node.command_range(former_range).toStream
+          (for {
+            (command, command_start) <- node.command_range(former_range)
             st = state.command_state(version, command)
             res = result(st)
             Text.Info(r0, a) <- st.markup.cumulate[A](
               (former_range - command_start).restrict(command.range), info, elements,
-              { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) })
-          } yield Text.Info(convert(r0 + command_start), a)
+              { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
+            ).iterator
+          } yield Text.Info(convert(r0 + command_start), a)).toList
         }
 
         def select_markup[A](range: Text.Range, elements: Option[Set[String]],
-          result: Command.State => Text.Markup => Option[A]): Stream[Text.Info[A]] =
+          result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
         {
           def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
           {

--- a/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 17:23:40 2013 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 19:59:58 2013 +0200
@@ -223,7 +223,7 @@
     to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
 
   def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
-    result: (A, Text.Markup) => Option[A]): Stream[Text.Info[A]] =
+    result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   {
     val notable: Elements => Boolean =
       result_elements match {
@@ -242,42 +242,42 @@
       if (changed) Some(y) else None
     }
 
-    def stream(
+    def traverse(
       last: Text.Offset,
-      stack: List[(Text.Info[A], Stream[(Text.Range, Entry)])]): Stream[Text.Info[A]] =
+      stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] =
     {
       stack match {
-        case (parent, (range, entry) #:: more) :: rest =>
+        case (parent, (range, entry) :: more) :: rest =>
           val subrange = range.restrict(root_range)
           val subtree =
             if (notable(entry.subtree_elements))
-              entry.subtree.overlapping(subrange).toStream
-            else Stream.empty
+              entry.subtree.overlapping(subrange).toList
+            else Nil
           val start = subrange.start
 
           (if (notable(entry.elements)) results(parent.info, entry) else None) match {
             case Some(res) =>
               val next = Text.Info(subrange, res)
-              val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
-              if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
+              val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
+              if (last < start) parent.restrict(Text.Range(last, start)) :: nexts
               else nexts
-            case None => stream(last, (parent, subtree #::: more) :: rest)
+            case None => traverse(last, (parent, subtree ::: more) :: rest)
           }
 
-        case (parent, Stream.Empty) :: rest =>
+        case (parent, Nil) :: rest =>
           val stop = parent.range.stop
-          val nexts = stream(stop, rest)
-          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
+          val nexts = traverse(stop, rest)
+          if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts
           else nexts
 
         case Nil =>
           val stop = root_range.stop
-          if (last < stop) Stream(Text.Info(Text.Range(last, stop), root_info))
-          else Stream.empty
+          if (last < stop) List(Text.Info(Text.Range(last, stop), root_info))
+          else Nil
       }
     }
-    stream(root_range.start,
-      List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
+    traverse(root_range.start,
+      List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
   }
 }
 

--- a/src/Tools/jEdit/src/fold_handling.scala	Wed Aug 07 17:23:40 2013 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Wed Aug 07 19:59:58 2013 +0200
@@ -31,7 +31,7 @@
         if (i < 0) 0
         else {
           rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match {
-            case d #:: _ => d
+            case d :: _ => d
             case _ => 0
           }
         }

--- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 17:23:40 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 19:59:58 2013 +0200
@@ -193,7 +193,7 @@
             if (highlight_include(elem.name))
               Some(Text.Info(snapshot.convert(info_range), highlight_color))
             else None
-        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
+        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
   }
 
 
@@ -244,7 +244,7 @@
             }
 
           case _ => None
-        }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
+        }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None }
   }
 
 
@@ -263,7 +263,7 @@
                 elem.name == Markup.SENDBACK)
               Some(Text.Info(snapshot.convert(info_range), elem))
             else None
-        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
+        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
 
 
   def command_results(range: Text.Range): Command.Results =
@@ -293,7 +293,7 @@
             Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
 
           case _ => None
-        }).toList.flatMap(_.info)
+        }).flatMap(_.info)
     if (results.isEmpty) None
     else {
       val r = Text.Range(results.head.range.start, results.last.range.stop)
@@ -366,7 +366,7 @@
             if (tooltips.isDefinedAt(name))
               Some(add(prev, r, (true, XML.Text(tooltips(name)))))
             else None
-        }).toList.map(_.info)
+        }).map(_.info)
 
     results.map(_.info).flatMap(_._2) match {
       case Nil => None
@@ -424,7 +424,7 @@
 
   private val squiggly_include = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
 
-  def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
+  def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
   {
     val results =
       snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ =>
@@ -482,9 +482,7 @@
 
 
   def output_messages(st: Command.State): List[XML.Tree] =
-  {
     st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
-  }
 
 
   private val background1_include =
@@ -492,9 +490,9 @@
       Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
       active_include
 
-  def background1(range: Text.Range): Stream[Text.Info[Color]] =
+  def background1(range: Text.Range): List[Text.Info[Color]] =
   {
-    if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
+    if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
     else
       for {
         Text.Info(r, result) <-
@@ -531,7 +529,7 @@
   }
 
 
-  def background2(range: Text.Range): Stream[Text.Info[Color]] =
+  def background2(range: Text.Range): List[Text.Info[Color]] =
     snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
       {
         case Text.Info(_, elem) =>
@@ -539,7 +537,7 @@
       })
 
 
-  def bullet(range: Text.Range): Stream[Text.Info[Color]] =
+  def bullet(range: Text.Range): List[Text.Info[Color]] =
     snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
       {
         case Text.Info(_, elem) =>
@@ -550,7 +548,7 @@
   private val foreground_include =
     Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ)
 
-  def foreground(range: Text.Range): Stream[Text.Info[Color]] =
+  def foreground(range: Text.Range): List[Text.Info[Color]] =
     snapshot.select_markup(range, Some(foreground_include), _ =>
       {
         case Text.Info(_, elem) =>
@@ -586,10 +584,9 @@
 
   private val text_color_elements = text_colors.keySet
 
-  def text_color(range: Text.Range, color: Color)
-      : Stream[Text.Info[Color]] =
+  def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   {
-    if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
+    if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
     else
       snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
         {
@@ -602,7 +599,7 @@
 
   private val fold_depth_include = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
 
-  def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
+  def fold_depth(range: Text.Range): List[Text.Info[Int]] =
     snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
       {
         case (depth, Text.Info(_, elem)) =>