# HG changeset patch
# User wenzelm
# Date 1355403138 -3600
# Node ID c94bba7906d23915651e3770bde793ed83fda647
# Parent  f496b2b7bafbb97362ea11ac215c58995a25a43f
identify dialogs via official serial and maintain as result message;
clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly;
cumulate_markup/select_markup depending on command state;
explicit Rendering.output_messages;
tuned source structure;

diff -r f496b2b7bafb -r c94bba7906d2 src/Pure/PIDE/active.ML
--- a/src/Pure/PIDE/active.ML	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/active.ML	Thu Dec 13 13:52:18 2012 +0100
@@ -12,7 +12,7 @@
   val sendback_markup_implicit: string -> string
   val sendback_markup: string -> string
   val dialog: unit -> (string -> Markup.T) * string future
-  val dialog_result: string -> string -> unit
+  val dialog_result: serial -> string -> unit
 end;
 
 structure Active: ACTIVE =
@@ -42,22 +42,20 @@
 
 (* dialog via document content *)
 
-val new_name = string_of_int o Synchronized.counter ();
-
-val dialogs = Synchronized.var "Active.dialogs" (Symtab.empty: string future Symtab.table);
+val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
 
 fun dialog () =
   let
-    val name = new_name ();
-    fun abort () = Synchronized.change dialogs (Symtab.delete_safe name);
+    val i = serial ();
+    fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
     val promise = Future.promise abort : string future;
-    val _ = Synchronized.change dialogs (Symtab.update_new (name, promise));
-    fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog name result);
+    val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
+    fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
   in (mk_markup, promise) end;
 
-fun dialog_result name result =
+fun dialog_result i result =
   Synchronized.change_result dialogs
-    (fn tab => (Symtab.lookup tab name, Symtab.delete_safe name tab))
+    (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
   |> (fn NONE => () | SOME promise => Future.fulfill promise result);
 
 end;
diff -r f496b2b7bafb -r c94bba7906d2 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Dec 13 13:52:18 2012 +0100
@@ -73,10 +73,10 @@
 
               val st0 = copy(results = results + (i -> message1))
               val st1 =
-                if (Protocol.is_tracing(message)) st0
-                else
+                if (Protocol.is_inlined(message))
                   (st0 /: Protocol.message_positions(command, message))(
                     (st, range) => st.add_markup(Text.Info(range, message2)))
+                else st0
 
               st1
             case _ => System.err.println("Ignored message without serial number: " + message); this
diff -r f496b2b7bafb -r c94bba7906d2 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Dec 13 13:52:18 2012 +0100
@@ -280,9 +280,9 @@
     def revert(range: Text.Range): Text.Range
     def eq_markup(other: Snapshot): Boolean
     def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
-      result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
+      result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
     def select_markup[A](range: Text.Range, elements: Option[Set[String]],
-      result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
+      result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
   }
 
   type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])]  // exec state assignment
@@ -506,29 +506,34 @@
             })
 
         def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
-          result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
+          result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
         {
           val former_range = revert(range)
           for {
             (command, command_start) <- node.command_range(former_range).toStream
-            Text.Info(r0, a) <- state.command_state(version, command).markup.
+            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))
-                  if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
-                    result((a, Text.Info(convert(r0 + command_start), b)))
+                  if res.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
+                    res((a, Text.Info(convert(r0 + command_start), b)))
                 })
           } yield Text.Info(convert(r0 + command_start), a)
         }
 
         def select_markup[A](range: Text.Range, elements: Option[Set[String]],
-          result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
+          result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
         {
-          val result1 =
+          def result1(st: Command.State) =
+          {
+            val res = result(st)
             new PartialFunction[(Option[A], Text.Markup), Option[A]] {
-              def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
-              def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
+              def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = res.isDefinedAt(arg._2)
+              def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(res(arg._2))
             }
+          }
           for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
             yield Text.Info(r, x)
         }
diff -r f496b2b7bafb -r c94bba7906d2 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Dec 13 13:52:18 2012 +0100
@@ -96,12 +96,6 @@
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
-  val graphviewN: string
-  val sendbackN: string
-  val paddingN: string
-  val padding_line: string * string
-  val dialogN: string val dialog: string -> string -> T
-  val intensifyN: string val intensify: T
   val taskN: string
   val acceptedN: string val accepted: T
   val forkedN: string val forked: T
@@ -122,6 +116,12 @@
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: T
+  val intensifyN: string val intensify: T
+  val graphviewN: string
+  val sendbackN: string
+  val paddingN: string
+  val padding_line: string * string
+  val dialogN: string val dialog: serial -> string -> T
   val functionN: string
   val assign_execs: Properties.T
   val removed_versions: Properties.T
@@ -339,20 +339,6 @@
 val (subgoalN, subgoal) = markup_elem "subgoal";
 
 
-(* active areas *)
-
-val graphviewN = "graphview";
-
-val sendbackN = "sendback";
-val paddingN = "padding";
-val padding_line = (paddingN, lineN);
-
-val dialogN = "dialog";
-fun dialog name result = (dialogN, [(nameN, name), ("result", result)]);
-
-val (intensifyN, intensify) = markup_elem "intensify";
-
-
 (* command status *)
 
 val taskN = "task";
@@ -385,6 +371,20 @@
 
 val (badN, bad) = markup_elem "bad";
 
+val (intensifyN, intensify) = markup_elem "intensify";
+
+
+(* active areas *)
+
+val graphviewN = "graphview";
+
+val sendbackN = "sendback";
+val paddingN = "padding";
+val padding_line = (paddingN, lineN);
+
+val dialogN = "dialog";
+fun dialog i result = (dialogN, [(serialN, print_int i), ("result", result)]);
+
 
 (* protocol message functions *)
 
diff -r f496b2b7bafb -r c94bba7906d2 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Dec 13 13:52:18 2012 +0100
@@ -213,30 +213,6 @@
   val SUBGOAL = "subgoal"
 
 
-  /* active areas */
-
-  val GRAPHVIEW = "graphview"
-
-  val SENDBACK = "sendback"
-  val PADDING = "padding"
-  val PADDING_LINE = (PADDING, LINE)
-
-  val DIALOG = "dialog"
-  val DIALOG_RESULT = "dialog_result"
-  val Result = new Properties.String("result")
-
-  object Dialog_Args
-  {
-    def unapply(props: Properties.T): Option[(String, String)] =
-      (props, props) match {
-        case (Markup.Name(name), Markup.Result(result)) => Some((name, result))
-        case _ => None
-      }
-  }
-
-  val INTENSIFY = "intensify"
-
-
   /* command status */
 
   val TASK = "task"
@@ -270,6 +246,7 @@
   val INIT = "init"
   val STATUS = "status"
   val REPORT = "report"
+  val RESULT = "result"
   val WRITELN = "writeln"
   val TRACING = "tracing"
   val WARNING = "warning"
@@ -298,6 +275,20 @@
 
   val BAD = "bad"
 
+  val INTENSIFY = "intensify"
+
+
+  /* active areas */
+
+  val GRAPHVIEW = "graphview"
+
+  val SENDBACK = "sendback"
+  val PADDING = "padding"
+  val PADDING_LINE = (PADDING, LINE)
+
+  val DIALOG = "dialog"
+  val Result = new Properties.String("result")
+
 
   /* protocol message functions */
 
diff -r f496b2b7bafb -r c94bba7906d2 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Dec 13 13:52:18 2012 +0100
@@ -77,8 +77,8 @@
 
 val _ =
   Isabelle_Process.protocol_command "Document.dialog_result"
-    (fn [name, result] =>
-      Active.dialog_result name result
+    (fn [serial, result] =>
+      Active.dialog_result (Markup.parse_int serial) result
         handle exn => if Exn.is_interrupt exn then () else reraise exn);
 
 val _ =
diff -r f496b2b7bafb -r c94bba7906d2 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Dec 13 13:52:18 2012 +0100
@@ -145,6 +145,15 @@
 
   /* specific messages */
 
+  def is_inlined(msg: XML.Tree): Boolean =
+    !(is_result(msg) || is_tracing(msg) || is_state(msg))
+
+  def is_result(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.RESULT, _), _) => true
+      case _ => false
+    }
+
   def is_tracing(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.TRACING, _), _) => true
@@ -152,6 +161,15 @@
       case _ => false
     }
 
+  def is_state(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.WRITELN, _),
+        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
+        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+      case _ => false
+    }
+
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true
@@ -166,14 +184,41 @@
       case _ => false
     }
 
-  def is_state(msg: XML.Tree): Boolean =
-    msg match {
-      case XML.Elem(Markup(Markup.WRITELN, _),
-        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
-      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
-        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
-      case _ => false
-    }
+
+  /* dialogs */
+
+  object Dialog_Args
+  {
+    def unapply(props: Properties.T): Option[(Document.ID, Long, String)] =
+      (props, props, props) match {
+        case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
+          Some((id, serial, result))
+        case _ => None
+      }
+  }
+
+  object Dialog
+  {
+    def unapply(tree: XML.Tree): Option[(Document.ID, Long, String)] =
+      tree match {
+        case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
+          Some((id, serial, result))
+        case _ => None
+      }
+  }
+
+  object Dialog_Result
+  {
+    def apply(serial: Long, result: String): XML.Elem =
+      XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result)))
+
+    def unapply(tree: XML.Tree): Option[(Long, String)] =
+      tree match {
+        case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result))) =>
+          Some((serial, result))
+        case _ => None
+      }
+  }
 
 
   /* reported positions */
@@ -205,7 +250,7 @@
       }
 
     val set = positions(Set.empty, message)
-    if (set.isEmpty && !is_state(message))
+    if (set.isEmpty)
       set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
     else set
   }
@@ -271,9 +316,9 @@
 
   /* dialog via document content */
 
-  def dialog_result(name: String, result: String)
+  def dialog_result(serial: Long, result: String)
   {
-    input("Document.dialog_result", name, result)
+    input("Document.dialog_result", Properties.Value.Long(serial), result)
   }
 
 
diff -r f496b2b7bafb -r c94bba7906d2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/ROOT.ML	Thu Dec 13 13:52:18 2012 +0100
@@ -98,6 +98,8 @@
 use "Concurrent/mailbox.ML";
 use "Concurrent/cache.ML";
 
+use "PIDE/active.ML";
+
 
 (* fundamental structures *)
 
@@ -251,7 +253,6 @@
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
 use "Thy/thy_syntax.ML";
-use "PIDE/active.ML";
 use "PIDE/command.ML";
 use "Isar/outer_syntax.ML";
 use "General/graph_display.ML";
diff -r f496b2b7bafb -r c94bba7906d2 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Dec 13 13:52:18 2012 +0100
@@ -26,7 +26,7 @@
   case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(edits: List[Document.Edit_Text])
-  case class Dialog_Result(id: Document.ID, name: String, result: String)
+  case class Dialog_Result(id: Document.ID, serial: Long, result: String)
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
@@ -420,13 +420,9 @@
 
           reply(())
 
-        case Session.Dialog_Result(id, name, result) if prover.isDefined =>
-          prover.get.dialog_result(name, result)
-
-          val dialog_result =
-            XML.Elem(Markup(Markup.DIALOG_RESULT, Markup.Name(name) ::: Markup.Result(result)), Nil)
-          handle_output(new Isabelle_Process.Output(
-            XML.Elem(Markup(Markup.STATUS, Position.Id(id)), List(dialog_result))))
+        case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
+          prover.get.dialog_result(serial, result)
+          handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(serial, result)))
 
         case Messages(msgs) =>
           msgs foreach {
@@ -479,6 +475,6 @@
   def update(edits: List[Document.Edit_Text])
   { session_actor !? Session.Raw_Edits(edits) }
 
-  def dialog_result(id: Document.ID, name: String, result: String)
-  { session_actor ! Session.Dialog_Result(id, name, result) }
+  def dialog_result(id: Document.ID, serial: Long, result: String)
+  { session_actor ! Session.Dialog_Result(id, serial, result) }
 }
diff -r f496b2b7bafb -r c94bba7906d2 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Tools/jEdit/src/active.scala	Thu Dec 13 13:52:18 2012 +0100
@@ -44,23 +44,6 @@
 
           if (!snapshot.is_outdated) {
             elem match {
-              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
-                props match {
-                  case Position.Id(exec_id) =>
-                    try_replace_command(exec_id, text)
-                  case _ =>
-                    if (props.exists(_ == Markup.PADDING_LINE))
-                      Isabelle.insert_line_padding(text_area, text)
-                    else text_area.setSelectedText(text)
-                }
-
-              case XML.Elem(Markup(Markup.DIALOG, props), _) =>
-                (props, props, props) match {
-                  case (Position.Id(id), Markup.Name(name), Markup.Result(result)) =>
-                    model.session.dialog_result(id, name, result)
-                  case _ =>
-                }
-
               case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) =>
                 default_thread_pool.submit(() =>
                   {
@@ -72,7 +55,24 @@
                     Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
                   })
 
+              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
+                props match {
+                  case Position.Id(exec_id) =>
+                    try_replace_command(exec_id, text)
+                  case _ =>
+                    if (props.exists(_ == Markup.PADDING_LINE))
+                      Isabelle.insert_line_padding(text_area, text)
+                    else text_area.setSelectedText(text)
+                }
+
               case _ =>
+                // FIXME pattern match problem in scala-2.9.2 (!??)
+                elem match {
+                  case Protocol.Dialog(id, serial, result) =>
+                    model.session.dialog_result(id, serial, result)
+
+                  case _ =>
+                }
             }
           }
         }
diff -r f496b2b7bafb -r c94bba7906d2 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Dec 13 13:52:18 2012 +0100
@@ -71,12 +71,8 @@
 
     val new_output =
       if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
-        // FIXME avoid intrusion of Protocol
-        // FIXME proper cumulation order!?
-        val status = new_state.status.filterNot(m => Protocol.command_status_markup(m.name))
-
-        val results = new_state.results.iterator.map(_._2).toList
-        results.map(tree => (tree /: status) { case (t, m) => XML.Elem(m, List(t)) })
+        val rendering = Rendering(new_snapshot, PIDE.options.value)
+        rendering.output_messages(new_state)
       }
       else current_output
 
diff -r f496b2b7bafb -r c94bba7906d2 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 13:52:18 2012 +0100
@@ -165,7 +165,7 @@
       val results =
         snapshot.cumulate_markup[(Protocol.Status, Int)](
           range, (Protocol.Status.init, 0),
-          Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR),
+          Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR), _ =>
           {
             case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
               if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
@@ -198,7 +198,7 @@
 
   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   {
-    snapshot.select_markup(range, Some(highlight_include),
+    snapshot.select_markup(range, Some(highlight_include), _ =>
         {
           case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
             Text.Info(snapshot.convert(info_range), highlight_color)
@@ -210,7 +210,7 @@
 
   def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
   {
-    snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
+    snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include), _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
@@ -250,11 +250,11 @@
   }
 
 
-  private val active_include = Set(Markup.SENDBACK, Markup.DIALOG, Markup.GRAPHVIEW)
+  private val active_include = Set(Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
 
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
-    snapshot.select_markup(range, Some(active_include),
-        {
+    snapshot.select_markup(range, Some(active_include), command_state =>
+        {  // FIXME inactive dialog
           case Text.Info(info_range, elem @ XML.Elem(markup, _))
           if active_include(markup.name) => Text.Info(snapshot.convert(info_range), elem)
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
@@ -264,7 +264,7 @@
   {
     val msgs =
       snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
-        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)),
+        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
         {
           case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
           if name == Markup.WRITELN ||
@@ -308,7 +308,7 @@
 
     val tips =
       snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
-        range, Text.Info(range, Nil), Some(tooltip_elements),
+        range, Text.Info(range, Nil), Some(tooltip_elements), _ =>
         {
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
             val kind1 = space_explode('_', kind).mkString(" ")
@@ -335,7 +335,7 @@
   def gutter_message(range: Text.Range): Option[Icon] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)),
+      snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)), _ =>
         {
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
             body match {
@@ -360,7 +360,7 @@
   {
     val results =
       snapshot.cumulate_markup[Int](range, 0,
-        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)),
+        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)), _ =>
         {
           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
           if name == Markup.WRITELN ||
@@ -386,7 +386,7 @@
   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, Some(messages_include),
+      snapshot.cumulate_markup[Int](range, 0, Some(messages_include), _ =>
         {
           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
           if name == Markup.WRITELN_MESSAGE ||
@@ -397,7 +397,7 @@
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
 
     val is_separator = pri > 0 &&
-      snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)),
+      snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
         {
           case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
         }).exists(_.info)
@@ -406,10 +406,16 @@
   }
 
 
+  def output_messages(st: Command.State): List[XML.Tree] =
+  {
+    st.results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
+  }
+
+
   private val background1_include =
     Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
-      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
-      Markup.DIALOG_RESULT ++ active_include
+      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
+      active_include
 
   def background1(range: Text.Range): Stream[Text.Info[Color]] =
   {
@@ -417,49 +423,47 @@
     else
       for {
         Text.Info(r, result) <-
-          snapshot.cumulate_markup[(Map[String, String], Option[Protocol.Status], Option[Color])](
-            range, (Map.empty, Some(Protocol.Status.init), None), Some(background1_include),
+          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
+            range, (Some(Protocol.Status.init), None), Some(background1_include), command_state =>
             {
-              case (((dialogs, Some(status), color), Text.Info(_, XML.Elem(markup, _))))
+              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
               if (Protocol.command_status_markup(markup.name)) =>
-                (dialogs, Some(Protocol.command_status(status, markup)), color)
-              case ((dialogs, _, _), Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
-                (dialogs, None, Some(bad_color))
-              case ((dialogs, _, _), Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
-                (dialogs, None, Some(intensify_color))
-              case ((dialogs, status, color), Text.Info(_,
-                XML.Elem(Markup(Markup.DIALOG_RESULT, Markup.Dialog_Args(name, result)), _))) =>
-                (dialogs + (name -> result), status, color)
-              case ((dialogs, _, _), Text.Info(_,
-                XML.Elem(Markup(Markup.DIALOG, Markup.Dialog_Args(name, result)), _))) =>
-                  if (dialogs.get(name) == Some(result))
-                    (dialogs, None, Some(active_result_color))
-                  else (dialogs, None, Some(active_color))
-              case ((dialogs, _, _), Text.Info(_, XML.Elem(Markup(name, _), _)))
-              if active_include(name) =>
-                (dialogs, None, Some(active_color))
+                (Some(Protocol.command_status(status, markup)), color)
+              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
+                (None, Some(bad_color))
+              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
+                (None, Some(intensify_color))
+              case (_, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
+                command_state.results.get(serial) match {
+                  case Some(Protocol.Dialog_Result(_, res)) if res == result =>
+                    (None, Some(active_result_color))
+                  case _ =>
+                    (None, Some(active_color))
+                }
+              case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
+                (None, Some(active_color))
             })
         color <-
           (result match {
-            case (_, Some(status), opt_color) =>
+            case (Some(status), opt_color) =>
               if (status.is_unprocessed) Some(unprocessed1_color)
               else if (status.is_running) Some(running1_color)
               else opt_color
-            case (_, _, opt_color) => opt_color
+            case (_, opt_color) => opt_color
           })
       } yield Text.Info(r, color)
   }
 
 
   def background2(range: Text.Range): Stream[Text.Info[Color]] =
-    snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)),
+    snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
       {
         case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
       })
 
 
   def foreground(range: Text.Range): Stream[Text.Info[Color]] =
-    snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)),
+    snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
       {
         case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
         case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
@@ -499,7 +503,7 @@
   {
     if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
     else
-      snapshot.cumulate_markup(range, color, Some(text_color_elements),
+      snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
         {
           case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
           if text_colors.isDefinedAt(m) => text_colors(m)