more careful handling of Dialog_Result, with active area and color feedback;
more formal type Command.Results;
propagate command results to output, which is required to resolve update of dialog state;
clarified Markup.message: retain uninterpreted messages;

--- a/src/Pure/PIDE/command.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -17,11 +17,14 @@
 {
   /** accumulated results from prover **/
 
+  type Results = SortedMap[Long, XML.Tree]
+  val empty_results: Results = SortedMap.empty
+
   sealed case class State(
-    val command: Command,
-    val status: List[Markup] = Nil,
-    val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
-    val markup: Markup_Tree = Markup_Tree.empty)
+    command: Command,
+    status: List[Markup] = Nil,
+    results: Results = empty_results,
+    markup: Markup_Tree = Markup_Tree.empty)
   {
     def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
       markup.to_XML(command.range, command.source, filter)
@@ -89,8 +92,8 @@
 
   type Span = List[Token]
 
-  def apply(id: Document.Command_ID, node_name: Document.Node.Name,
-    span: Span, markup: Markup_Tree): Command =
+  def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span,
+    results: Results = empty_results, markup: Markup_Tree = Markup_Tree.empty): Command =
   {
     val source: String =
       span match {
@@ -107,21 +110,23 @@
       i += n
     }
 
-    new Command(id, node_name, span1.toList, source, markup)
+    new Command(id, node_name, span1.toList, source, results, markup)
   }
 
-  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil, Markup_Tree.empty)
+  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
 
-  def unparsed(id: Document.Command_ID, source: String, markup: Markup_Tree): Command =
-    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), markup)
+  def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree)
+      : Command =
+    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
 
-  def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty)
+  def unparsed(source: String): Command =
+    unparsed(Document.no_id, source, empty_results, Markup_Tree.empty)
 
-  def rich_text(id: Document.Command_ID, body: XML.Body): Command =
+  def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
   {
     val text = XML.content(body)
     val markup = Markup_Tree.from_XML(body)
-    unparsed(id, text, markup)
+    unparsed(id, text, results, markup)
   }
 
 
@@ -152,6 +157,7 @@
     val node_name: Document.Node.Name,
     val span: Command.Span,
     val source: String,
+    val init_results: Command.Results,
     val init_markup: Markup_Tree)
 {
   /* classification */
@@ -188,5 +194,6 @@
 
   /* accumulated results */
 
-  val init_state: Command.State = Command.State(this, markup = init_markup)
+  val init_state: Command.State =
+    Command.State(this, results = init_results, markup = init_markup)
 }

--- a/src/Pure/PIDE/markup.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -264,8 +264,7 @@
 
   val message: String => String =
     Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
-        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
-      .withDefault((name: String) => name + "_message")
+        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).withDefault((s: String) => s)
 
   val Return_Code = new Properties.Int("return_code")
 

--- a/src/Pure/PIDE/protocol.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -209,13 +209,15 @@
 
   object Dialog_Result
   {
-    def apply(serial: Long, result: String): XML.Elem =
-      XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result)))
+    def apply(id: Document.ID, serial: Long, result: String): XML.Elem =
+    {
+      val props = Position.Id(id) ::: Markup.Serial(serial)
+      XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
+    }
 
-    def unapply(tree: XML.Tree): Option[(Long, String)] =
+    def unapply(tree: XML.Tree): Option[String] =
       tree match {
-        case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result))) =>
-          Some((serial, result))
+        case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
         case _ => None
       }
   }

--- a/src/Pure/System/session.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -422,7 +422,7 @@
 
         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)))
+          handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
 
         case Messages(msgs) =>
           msgs foreach {

--- a/src/Pure/Thy/thy_syntax.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty)))
+      spans.foreach(span => add(Command(Document.no_id, node_name, span)))
       result()
     }
   }
@@ -226,7 +226,7 @@
         commands
       case cmd :: _ =>
         val hook = commands.prev(cmd)
-        val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty))
+        val inserted = spans2.map(span => Command(Document.new_id(), name, span))
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -65,7 +65,7 @@
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
           {
             val rendering = Rendering(snapshot, PIDE.options.value)
-            new Pretty_Tooltip(view, parent, rendering, x, y, body)
+            new Pretty_Tooltip(view, parent, rendering, x, y, Command.empty_results, body)
             null
           }
         }

--- a/src/Tools/jEdit/src/info_dockable.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -26,22 +26,24 @@
   /* implicit arguments -- owned by Swing thread */
 
   private var implicit_snapshot = Document.State.init.snapshot()
+  private var implicit_results = Command.empty_results
   private var implicit_info: XML.Body = Nil
 
-  private def set_implicit(snapshot: Document.Snapshot, info: XML.Body)
+  private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
   {
     Swing_Thread.require()
 
     implicit_snapshot = snapshot
+    implicit_results = results
     implicit_info = info
   }
 
   private def reset_implicit(): Unit =
-    set_implicit(Document.State.init.snapshot(), Nil)
+    set_implicit(Document.State.init.snapshot(), Command.empty_results, Nil)
 
-  def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
+  def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
   {
-    set_implicit(snapshot, info)
+    set_implicit(snapshot, results, info)
     view.getDockableWindowManager.floatDockableWindow("isabelle-info")
   }
 }
@@ -57,11 +59,12 @@
   private var zoom_factor = 100
 
   private val snapshot = Info_Dockable.implicit_snapshot
+  private val results = Info_Dockable.implicit_results
   private val info = Info_Dockable.implicit_info
 
   private val window_focus_listener =
     new WindowFocusListener {
-      def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, info) }
+      def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, results, info) }
       def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
     }
 
@@ -71,7 +74,7 @@
   private val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
-  pretty_text_area.update(snapshot, info)
+  pretty_text_area.update(snapshot, results, info)
 
   private def handle_resize()
   {

--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -77,7 +77,7 @@
       else current_output
 
     if (new_output != current_output)
-      pretty_text_area.update(new_snapshot, Pretty.separate(new_output))
+      pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
 
     current_snapshot = new_snapshot
     current_state = new_state
@@ -152,7 +152,8 @@
   private val detach = new Button("Detach") {
     reactions += {
       case ButtonClicked(_) =>
-        Info_Dockable(view, current_snapshot, Pretty.separate(current_output))
+        Info_Dockable(view, current_snapshot,
+          current_state.results, Pretty.separate(current_output))
     }
   }
   detach.tooltip = "Detach window with static copy of current output"

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -21,18 +21,18 @@
 
 object Pretty_Text_Area
 {
-  private def text_rendering(base_snapshot: Document.Snapshot, formatted_body: XML.Body):
-    (String, Rendering) =
+  private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
+    formatted_body: XML.Body): (String, Rendering) =
   {
-    val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body)
+    val (text, state) = Pretty_Text_Area.document_state(base_snapshot, base_results, formatted_body)
     val rendering = Rendering(state.snapshot(), PIDE.options.value)
     (text, rendering)
   }
 
-  private def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
-    : (String, Document.State) =
+  private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
+    formatted_body: XML.Body): (String, Document.State) =
   {
-    val command = Command.rich_text(Document.new_id(), formatted_body)
+    val command = Command.rich_text(Document.new_id(), base_results, formatted_body)
     val node_name = command.node_name
     val edits: List[Document.Edit_Text] =
       List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
@@ -62,8 +62,9 @@
   private var current_font_size: Int = 12
   private var current_body: XML.Body = Nil
   private var current_base_snapshot = Document.State.init.snapshot()
+  private var current_base_results = Command.empty_results
   private var current_rendering: Rendering =
-    Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2
+    Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
   private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
 
   private val rich_text_area =
@@ -84,12 +85,14 @@
       val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
 
       val base_snapshot = current_base_snapshot
+      val base_results = current_base_results
       val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
 
       future_rendering.map(_.cancel(true))
       future_rendering = Some(default_thread_pool.submit(() =>
         {
-          val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
+          val (text, rendering) =
+            Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body)
           Simple_Thread.interrupted_exception()
 
           Swing_Thread.later {
@@ -115,12 +118,13 @@
     refresh()
   }
 
-  def update(base_snapshot: Document.Snapshot, body: XML.Body)
+  def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
   {
     Swing_Thread.require()
     require(!base_snapshot.is_outdated)
 
     current_base_snapshot = base_snapshot
+    current_base_results = base_results
     current_body = body
     refresh()
   }

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -25,7 +25,9 @@
   view: View,
   parent: JComponent,
   rendering: Rendering,
-  mouse_x: Int, mouse_y: Int, body: XML.Body)
+  mouse_x: Int, mouse_y: Int,
+  results: Command.Results,
+  body: XML.Body)
   extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view)
 {
   window =>
@@ -70,7 +72,7 @@
   pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
   pretty_text_area.resize(Rendering.font_family(),
     Rendering.font_size("jedit_tooltip_font_scale").round)
-  pretty_text_area.update(rendering.snapshot, body)
+  pretty_text_area.update(rendering.snapshot, results, body)
 
   pretty_text_area.registerKeyboardAction(action_listener, "close_all",
     KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
@@ -92,7 +94,9 @@
     tooltip = "Detach tooltip window"
     listenTo(mouse.clicks)
     reactions += {
-      case _: MouseClicked => Info_Dockable(view, rendering.snapshot, body); window.dispose()
+      case _: MouseClicked =>
+        Info_Dockable(view, rendering.snapshot, results, body)
+        window.dispose()
     }
   }
 

--- a/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -254,16 +254,20 @@
 
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
     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)
+        {
+          case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
+          if !command_state.results.isDefinedAt(serial) =>
+            Text.Info(snapshot.convert(info_range), elem)
+          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
+          if name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
+            Text.Info(snapshot.convert(info_range), elem)
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
 
 
   def tooltip_message(range: Text.Range): XML.Body =
   {
     val msgs =
-      snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
+      snapshot.cumulate_markup[Command.Results](range, Command.empty_results,
         Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
         {
           case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
@@ -433,12 +437,17 @@
                 (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 (acc, Text.Info(_, elem @ XML.Elem(Markup(Markup.DIALOG, _), _))) =>
+                // FIXME pattern match problem in scala-2.9.2 (!??)
+                elem match {
+                  case 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 _ => acc
                 }
               case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
                 (None, Some(active_color))

--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -204,13 +204,14 @@
           JEdit_Lib.pixel_range(text_area, x, y) match {
             case None =>
             case Some(range) =>
+              // FIXME cumulate results!?
               val tip =
                 if (control) rendering.tooltip(range)
                 else rendering.tooltip_message(range)
               if (!tip.isEmpty) {
                 val painter = text_area.getPainter
                 val y1 = y + painter.getFontMetrics.getHeight / 2
-                new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
+                new Pretty_Tooltip(view, painter, rendering, x, y1, Command.empty_results, tip)
               }
           }
         }