clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;

--- a/NEWS	Thu Feb 20 16:08:39 2014 +0100
+++ b/NEWS	Thu Feb 20 16:56:51 2014 +0100
@@ -340,6 +340,15 @@
     intervals.
 
 
+*** Scala ***
+
+* The signature and semantics of Document.Snapshot.cumulate_markup /
+select_markup have been clarified.  Markup is now traversed in the
+order of reports given by the prover: later markup is usually more
+specific and may override results accumulated so far.  The elements
+guard is mandatory and checked precisely.  Subtle INCOMPATIBILITY.
+
+
 *** ML ***
 
 * Proper context discipline for read_instantiate and instantiate_tac:

--- a/src/Pure/PIDE/command.scala	Thu Feb 20 16:08:39 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Feb 20 16:56:51 2014 +0100
@@ -90,8 +90,7 @@
           (this /: msgs)((state, msg) =>
             msg match {
               case elem @ XML.Elem(markup, Nil) =>
-                state.add_status(markup)
-                  .add_markup("", Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
+                state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem))
 
               case _ =>
                 System.err.println("Ignored status message: " + msg)

--- a/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 16:08:39 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 16:56:51 2014 +0100
@@ -230,7 +230,7 @@
       var y = x
       var changed = false
       for {
-        elem <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
+        elem <- entry.markup
         if elements(elem.name)
         y1 <- result(y, Text.Info(entry.range, elem))
       } { y = y1; changed = true }

--- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:08:39 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:56:51 2014 +0100
@@ -298,18 +298,18 @@
 
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
-    snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
-      range, Nil, hyperlink_elements, _ =>
+    snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]](
+      range, Vector.empty, hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             val link = PIDE.editor.hyperlink_file(jedit_file)
-            Some(Text.Info(snapshot.convert(info_range), link) :: links)
+            Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
             val link = PIDE.editor.hyperlink_url(name)
-            Some(Text.Info(snapshot.convert(info_range), link) :: links)
+            Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
           if !props.exists(
@@ -323,7 +323,7 @@
                 case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
                 case _ => None
               }
-            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
+            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
             val opt_link =
@@ -332,15 +332,15 @@
                 case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
                 case _ => None
               }
-            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
+            opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))
 
           case _ => None
-        }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None }
+        }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   }
 
 
   private val active_elements =
-    Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
+    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE)
 
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
     snapshot.select_markup(range, active_elements, command_state =>
@@ -348,6 +348,7 @@
         case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
         if !command_state.results.defined(serial) =>
           Some(Text.Info(snapshot.convert(info_range), elem))
+
         case Text.Info(info_range, elem) =>
           if (elem.name == Markup.BROWSER ||
               elem.name == Markup.GRAPHVIEW ||
@@ -420,17 +421,19 @@
 
   def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
   {
-    def add(prev: Text.Info[(Timing, List[(Boolean, XML.Tree)])],
-      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, List[(Boolean, XML.Tree)])] =
+    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
+      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
     {
       val r = snapshot.convert(r0)
       val (t, info) = prev.info
-      if (prev.range == r) Text.Info(r, (t, p :: info)) else Text.Info(r, (t, List(p)))
+      if (prev.range == r)
+        Text.Info(r, (t, info :+ p))
+      else Text.Info(r, (t, Vector(p)))
     }
 
     val results =
-      snapshot.cumulate_markup[Text.Info[(Timing, List[(Boolean, XML.Tree)])]](
-        range, Text.Info(range, (Timing.zero, Nil)), tooltip_elements, _ =>
+      snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
+        range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
         {
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
             Some(Text.Info(r, (t1 + t2, info)))
@@ -462,7 +465,7 @@
             else None
         }).map(_.info)
 
-    results.map(_.info).flatMap(_._2) match {
+    results.map(_.info).flatMap(res => res._2.toList) match {
       case Nil => None
       case tips =>
         val r = Text.Range(results.head.range.start, results.last.range.stop)