# HG changeset patch
# User wenzelm
# Date 1325936386 -3600
# Node ID 793cecd4ffc0628db0fa5da04004f25513bb0728
# Parent  913ea585efdca0b589e8fb30b84288a6ba4a27f9
accumulate status as regular markup for command range;
tuned signature;

diff -r 913ea585efdc -r 793cecd4ffc0 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Jan 07 11:45:53 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Jan 07 12:39:46 2012 +0100
@@ -23,27 +23,20 @@
     val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
     val markup: Markup_Tree = Markup_Tree.empty)
   {
-    /* content */
-
-    def add_status(st: Markup): State = copy(status = st :: status)
-    def add_markup(m: Text.Markup): State = copy(markup = markup + m)
-    def add_result(serial: Long, result: XML.Tree): State =
-      copy(results = results + (serial -> result))
+    /* accumulate content */
 
-    def root_info: Text.Markup =
-      Text.Info(command.range,
-        XML.Elem(Markup(Isabelle_Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
-    def root_markup: Markup_Tree = markup + root_info
+    private def add_status(st: Markup): State = copy(status = st :: status)
+    private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
 
-
-    /* message dispatch */
-
-    def accumulate(message: XML.Elem): Command.State =
+    def + (message: XML.Elem): Command.State =
       message match {
         case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
             msg match {
-              case XML.Elem(markup, Nil) => state.add_status(markup)
+              case elem @ XML.Elem(markup, Nil) =>
+                val info: Text.Markup = Text.Info(command.range, elem)
+                state.add_status(markup).add_markup(info)
+
               case _ => System.err.println("Ignored status message: " + msg); state
             })
 
@@ -64,13 +57,13 @@
           atts match {
             case Isabelle_Markup.Serial(i) =>
               val result = XML.Elem(Markup(name, Position.purge(atts)), body)
-              val st0 = add_result(i, result)
+              val st0 = copy(results = results + (i -> result))
               val st1 =
                 if (Protocol.is_tracing(message)) st0
                 else
                   (st0 /: Protocol.message_positions(command, message))(
                     (st, range) => st.add_markup(Text.Info(range, result)))
-              val st2 = (st1 /: Protocol.message_reports(message))(_ accumulate _)
+              val st2 = (st1 /: Protocol.message_reports(message))(_ + _)
               st2
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
diff -r 913ea585efdc -r 793cecd4ffc0 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Jan 07 11:45:53 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Jan 07 12:39:46 2012 +0100
@@ -325,12 +325,12 @@
     def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
         case Some(st) =>
-          val new_st = st.accumulate(message)
+          val new_st = st + message
           (new_st, copy(execs = execs + (id -> new_st)))
         case None =>
           commands.get(id) match {
             case Some(st) =>
-              val new_st = st.accumulate(message)
+              val new_st = st + message
               (new_st, copy(commands = commands + (id -> new_st)))
             case None => fail
           }
diff -r 913ea585efdc -r 793cecd4ffc0 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Jan 07 11:45:53 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Jan 07 12:39:46 2012 +0100
@@ -152,7 +152,7 @@
     val root = data.root
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
-      snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Markup) =>
+      snapshot.command_state(command).markup.swing_tree(root)((info: Text.Markup) =>
           {
             val range = info.range + command_start
             val content = command.source(info.range).replace('\n', ' ')