# HG changeset patch
# User wenzelm
# Date 1355485207 -3600
# Node ID bd145273e7c67cab612c6d04c15e41392d87602f
# Parent  0799339fea0f3cdf961a3c6f1bf3b48a68fec48b# Parent  4a389d115b4fa1eaf3c6ed39a5d38f531666d474
merged

diff -r 0799339fea0f -r bd145273e7c6 NEWS
--- a/NEWS	Thu Dec 13 23:47:01 2012 +0100
+++ b/NEWS	Fri Dec 14 12:40:07 2012 +0100
@@ -69,10 +69,9 @@
 * More efficient painting and improved reactivity when editing large
 files.  More scalable management of formal document content.
 
-* Smarter handling of tracing messages: output window informs about
-accumulated messages; prover transactions are limited to emit maximum
-amount of output, before being canceled (cf. system option
-"editor_tracing_limit_MB").  This avoids swamping the front-end with
+* Smarter handling of tracing messages: prover process pauses after
+certain number of messages per command transaction, with some user
+dialog to stop or continue.  This avoids swamping the front-end with
 potentially infinite message streams.
 
 * More plugin options and preferences, based on Isabelle/Scala.  The
diff -r 0799339fea0f -r bd145273e7c6 etc/options
--- a/etc/options	Thu Dec 13 23:47:01 2012 +0100
+++ b/etc/options	Fri Dec 14 12:40:07 2012 +0100
@@ -96,5 +96,5 @@
 option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
 
-option editor_tracing_limit_MB : real = 2.5
-  -- "maximum tracing volume for each command transaction"
+option editor_tracing_messages : int = 100
+  -- "initial number of tracing messages for each command transaction"
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/General/output.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -34,6 +34,7 @@
     val prompt_fn: (output -> unit) Unsynchronized.ref
     val status_fn: (output -> unit) Unsynchronized.ref
     val report_fn: (output -> unit) Unsynchronized.ref
+    val result_fn: (serial * output -> unit) Unsynchronized.ref
     val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
   end
   val urgent_message: string -> unit
@@ -42,8 +43,8 @@
   val prompt: string -> unit
   val status: string -> unit
   val report: string -> unit
+  val result: serial * string -> unit
   val protocol_message: Properties.T -> string -> unit
-  exception TRACING_LIMIT of int
 end;
 
 structure Output: OUTPUT =
@@ -97,6 +98,7 @@
   val prompt_fn = Unsynchronized.ref physical_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
+  val result_fn = Unsynchronized.ref (fn _: serial * output => ());
   val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
     Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
 end;
@@ -110,10 +112,9 @@
 fun prompt s = ! Private_Hooks.prompt_fn (output s);
 fun status s = ! Private_Hooks.status_fn (output s);
 fun report s = ! Private_Hooks.report_fn (output s);
+fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
 fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
 
-exception TRACING_LIMIT of int;
-
 end;
 
 structure Basic_Output: BASIC_OUTPUT = Output;
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/Isar/runtime.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -76,7 +76,6 @@
             | TOPLEVEL_ERROR => "Error"
             | ERROR msg => msg
             | Fail msg => raised exn "Fail" [msg]
-            | Output.TRACING_LIMIT n => "Tracing limit exceeded: " ^ string_of_int n
             | THEORY (msg, thys) =>
                 raised exn "THEORY" (msg :: map Context.str_of_thy thys)
             | Ast.AST (msg, asts) =>
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/PIDE/active.ML
--- a/src/Pure/PIDE/active.ML	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/active.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -11,27 +11,57 @@
   val markup: string -> string -> string
   val sendback_markup_implicit: string -> string
   val sendback_markup: string -> string
+  val dialog: unit -> (string -> Markup.T) * string future
+  val dialog_text: unit -> (string -> string) * string future
+  val dialog_result: serial -> string -> unit
 end;
 
 structure Active: ACTIVE =
 struct
 
+(* active markup *)
+
+fun explicit_id () =
+  (case Position.get_id (Position.thread_data ()) of
+    SOME id => [(Markup.idN, id)]
+  | NONE => []);
+
 fun make_markup name {implicit, properties} =
   (name, [])
-  |> not implicit ? (fn markup =>
-      let
-        val props =
-          (case Position.get_id (Position.thread_data ()) of
-            SOME id => [(Markup.idN, id)]
-          | NONE => []);
-      in Markup.properties props markup end)
+  |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
   |> Markup.properties properties;
 
 fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
 fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
 
+
+(* sendback area *)
+
 val sendback_markup_implicit = markup_implicit Markup.sendbackN;
 val sendback_markup = markup Markup.sendbackN;
 
+
+(* dialog via document content *)
+
+val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
+
+fun dialog () =
+  let
+    val i = serial ();
+    fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
+    val promise = Future.promise abort : string future;
+    val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
+    fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
+  in (result_markup, promise) end;
+
+fun dialog_text () =
+  let val (markup, promise) = dialog ()
+  in (fn s => Markup.markup (markup s) s, promise) end;
+
+fun dialog_result i result =
+  Synchronized.change_result dialogs
+    (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
+  |> (fn NONE => () | SOME promise => Future.fulfill promise result);
+
 end;
 
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Dec 14 12:40:07 2012 +0100
@@ -17,11 +17,38 @@
 {
   /** accumulated results from prover **/
 
+  /* results */
+
+  object Results
+  {
+    val empty = new Results(SortedMap.empty)
+    def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
+  }
+
+  final class Results private(rep: SortedMap[Long, XML.Tree])
+  {
+    def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
+    def get(serial: Long): Option[XML.Tree] = rep.get(serial)
+    def entries: Iterator[(Long, XML.Tree)] = rep.iterator
+
+    def + (entry: (Long, XML.Tree)): Results =
+      if (defined(entry._1)) this
+      else new Results(rep + entry)
+
+    def ++ (other: Results): Results =
+      if (this eq other) this
+      else if (rep.isEmpty) other
+      else (this /: other.entries)(_ + _)
+  }
+
+
+  /* state */
+
   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 = Results.empty,
+    markup: Markup_Tree = Markup_Tree.empty)
   {
     def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
       markup.to_XML(command.range, command.source, filter)
@@ -38,7 +65,8 @@
           (this /: msgs)((state, msg) =>
             msg match {
               case elem @ XML.Elem(markup, Nil) =>
-                state.add_status(markup).add_markup(Text.Info(command.proper_range, elem))
+                state.add_status(markup)
+                  .add_markup(Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
 
               case _ => System.err.println("Ignored status message: " + msg); state
             })
@@ -72,10 +100,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
@@ -88,8 +116,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 = Results.empty, markup: Markup_Tree = Markup_Tree.empty): Command =
   {
     val source: String =
       span match {
@@ -106,21 +134,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, Results.empty, 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)
   }
 
 
@@ -151,6 +181,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 */
@@ -187,5 +218,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)
 }
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 14 12:40:07 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 0799339fea0f -r bd145273e7c6 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -96,11 +96,6 @@
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
-  val paddingN: string
-  val padding_line: string * string
-  val sendbackN: string
-  val graphviewN: string
-  val intensifyN: string val intensify: T
   val taskN: string
   val acceptedN: string val accepted: T
   val forkedN: string val forked: T
@@ -111,6 +106,7 @@
   val serialN: string
   val initN: string
   val statusN: string
+  val resultN: string
   val writelnN: string
   val tracingN: string
   val warningN: string
@@ -121,6 +117,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
@@ -338,17 +340,6 @@
 val (subgoalN, subgoal) = markup_elem "subgoal";
 
 
-(* active areads *)
-
-val sendbackN = "sendback";
-val graphviewN = "graphview";
-
-val paddingN = "padding";
-val padding_line = (paddingN, lineN);
-
-val (intensifyN, intensify) = markup_elem "intensify";
-
-
 (* command status *)
 
 val taskN = "task";
@@ -367,6 +358,7 @@
 
 val initN = "init";
 val statusN = "status";
+val resultN = "result";
 val writelnN = "writeln";
 val tracingN = "tracing";
 val warningN = "warning";
@@ -381,6 +373,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), (resultN, result)]);
+
 
 (* protocol message functions *)
 
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Dec 14 12:40:07 2012 +0100
@@ -213,17 +213,6 @@
   val SUBGOAL = "subgoal"
 
 
-  /* active areas */
-
-  val SENDBACK = "sendback"
-  val GRAPHVIEW = "graphview"
-
-  val PADDING = "padding"
-  val PADDING_LINE = (PADDING, LINE)
-
-  val INTENSIFY = "intensify"
-
-
   /* command status */
 
   val TASK = "task"
@@ -257,6 +246,7 @@
   val INIT = "init"
   val STATUS = "status"
   val REPORT = "report"
+  val RESULT = "result"
   val WRITELN = "writeln"
   val TRACING = "tracing"
   val WARNING = "warning"
@@ -274,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")
 
@@ -285,6 +274,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 0799339fea0f -r bd145273e7c6 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -60,7 +60,7 @@
               |> YXML.string_of_body);
 
         val _ = List.app Future.cancel_group (Goal.reset_futures ());
-        val _ = Isabelle_Process.reset_tracing_limits ();
+        val _ = Isabelle_Process.reset_tracing ();
         val _ = Document.start_execution state';
       in state' end));
 
@@ -76,6 +76,12 @@
       in state1 end));
 
 val _ =
+  Isabelle_Process.protocol_command "Document.dialog_result"
+    (fn [serial, result] =>
+      Active.dialog_result (Markup.parse_int serial) result
+        handle exn => if Exn.is_interrupt exn then () else reraise exn);
+
+val _ =
   Isabelle_Process.protocol_command "Document.invoke_scala"
     (fn [id, tag, res] =>
       Invoke_Scala.fulfill_method id tag res
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Dec 14 12:40:07 2012 +0100
@@ -106,7 +106,7 @@
         val status = command_status(st.status)
         if (status.is_running) running += 1
         else if (status.is_finished) {
-          if (st.results.exists(p => is_warning(p._2))) warned += 1
+          if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
           else finished += 1
         }
         else if (status.is_failed) failed += 1
@@ -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,15 +184,44 @@
       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(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[String] =
+      tree match {
+        case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
+        case _ => None
+      }
+  }
+
 
   /* reported positions */
 
@@ -205,7 +252,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
   }
@@ -269,6 +316,14 @@
   }
 
 
+  /* dialog via document content */
+
+  def dialog_result(serial: Long, result: String)
+  {
+    input("Document.dialog_result", Properties.Value.Long(serial), result)
+  }
+
+
   /* method invocation service */
 
   def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/ROOT.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -63,7 +63,6 @@
 
 use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
-use "PIDE/active.ML";
 
 use "General/graph.ML";
 
@@ -99,6 +98,8 @@
 use "Concurrent/mailbox.ML";
 use "Concurrent/cache.ML";
 
+use "PIDE/active.ML";
+
 
 (* fundamental structures *)
 
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -17,8 +17,8 @@
 sig
   val is_active: unit -> bool
   val protocol_command: string -> (string list -> unit) -> unit
-  val tracing_limit: int Unsynchronized.ref;
-  val reset_tracing_limits: unit -> unit
+  val tracing_messages: int Unsynchronized.ref;
+  val reset_tracing: unit -> unit
   val crashes: exn list Synchronized.var
   val init_fifos: string -> string -> unit
   val init_socket: string -> unit
@@ -63,24 +63,43 @@
 end;
 
 
-(* tracing limit *)
+(* restricted tracing messages *)
 
-val tracing_limit = Unsynchronized.ref 1000000;
+val tracing_messages = Unsynchronized.ref 100;
 
-val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
+val command_tracing_messages =
+  Synchronized.var "command_tracing_messages" (Inttab.empty: int Inttab.table);
 
-fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty);
+fun reset_tracing () =
+  Synchronized.change command_tracing_messages (K Inttab.empty);
 
-fun update_tracing_limits msg =
+fun update_tracing () =
   (case Position.get_id (Position.thread_data ()) of
     NONE => ()
   | SOME id =>
-      Synchronized.change tracing_limits (fn tab =>
-        let
-          val i = Markup.parse_int id;
-          val n = the_default 0 (Inttab.lookup tab i) + size msg;
-          val _ = if n > ! tracing_limit then raise Output.TRACING_LIMIT n else ();
-        in Inttab.update (i, n) tab end));
+      let
+        val i = Markup.parse_int id;
+        val (n, ok) =
+          Synchronized.change_result command_tracing_messages (fn tab =>
+            let
+              val n = the_default 0 (Inttab.lookup tab i) + 1;
+              val ok = n <= ! tracing_messages;
+            in ((n, ok), Inttab.update (i, n) tab) end);
+      in
+        if ok then ()
+        else
+          let
+            val (text, promise) = Active.dialog_text ();
+            val _ =
+              writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
+                text "10" ^ ", " ^ text "100" ^ ", " ^ text "1000" ^ " messages?")
+            val m = Markup.parse_int (Future.join promise)
+              handle Fail _ => error "Stopped";
+          in
+            Synchronized.change command_tracing_messages
+              (Inttab.map_default (i, 0) (fn k => k - m))
+          end
+      end);
 
 
 (* message channels *)
@@ -126,10 +145,12 @@
   in
     Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN;
     Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN;
+    Output.Private_Hooks.result_fn :=
+      (fn (i, s) => standard_message mbox (SOME i) Markup.resultN s);
     Output.Private_Hooks.writeln_fn :=
       (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
     Output.Private_Hooks.tracing_fn :=
-      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) Markup.tracingN s));
+      (fn s => (update_tracing (); standard_message mbox (SOME (serial ())) Markup.tracingN s));
     Output.Private_Hooks.warning_fn :=
       (fn s => standard_message mbox (SOME (serial ())) Markup.warningN s);
     Output.Private_Hooks.error_fn :=
@@ -224,8 +245,7 @@
         then Multithreading.max_threads := 2 else ();
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
         Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
-        tracing_limit :=
-          Real.round (Options.real options "editor_tracing_limit_MB" * 1024.0 * 1024.0)
+        tracing_messages := Options.int options "editor_tracing_messages"
       end);
 
 end;
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/System/session.scala	Fri Dec 14 12:40:07 2012 +0100
@@ -26,6 +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, serial: Long, result: String)
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
@@ -419,6 +420,10 @@
 
           reply(())
 
+        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(id, serial, result)))
+
         case Messages(msgs) =>
           msgs foreach {
             case input: Isabelle_Process.Input =>
@@ -469,4 +474,7 @@
 
   def update(edits: List[Document.Edit_Text])
   { session_actor !? Session.Raw_Edits(edits) }
+
+  def dialog_result(id: Document.ID, serial: Long, result: String)
+  { session_actor ! Session.Dialog_Result(id, serial, result) }
 }
diff -r 0799339fea0f -r bd145273e7c6 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Dec 14 12:40:07 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)
     }
   }
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/etc/options	Fri Dec 14 12:40:07 2012 +0100
@@ -43,6 +43,7 @@
 option hyperlink_color : string = "000000FF"
 option active_color : string = "DCDCDCFF"
 option active_hover_color : string = "9DC75DFF"
+option active_result_color : string = "999966FF"
 option keyword1_color : string = "006699FF"
 option keyword2_color : string = "009966FF"
 
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/active.scala	Fri Dec 14 12:40:07 2012 +0100
@@ -44,16 +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.GRAPHVIEW, Position.Id(exec_id)), body) =>
                 default_thread_pool.submit(() =>
                   {
@@ -65,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 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Fri Dec 14 12:40:07 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.Results.empty, body)
             null
           }
         }
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Dec 14 12:40:07 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.Results.empty
   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.Results.empty, 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()
   {
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Fri Dec 14 12:40:07 2012 +0100
@@ -45,7 +45,7 @@
       "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
       "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
       "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
-      "editor_tracing_limit_MB", "editor_update_delay")
+      "editor_tracing_messages", "editor_update_delay")
 
   relevant_options.foreach(PIDE.options.value.check_name _)
 
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Fri Dec 14 12:40:07 2012 +0100
@@ -191,8 +191,8 @@
 isabelle.control-bold.shortcut=C+e RIGHT
 isabelle.control-isub.label=Control subscript
 isabelle.control-isub.shortcut=C+e DOWN
-isabelle.control-isup.label=Control superscript
-isabelle.control-isup.shortcut=C+e UP
+isabelle.control-sup.label=Control superscript
+isabelle.control-sup.shortcut=C+e UP
 isabelle.control-reset.label=Control reset
 isabelle.control-reset.shortcut=C+e LEFT
 isabelle.decrease-font-size.label=Decrease font size
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Dec 14 12:40:07 2012 +0100
@@ -70,12 +70,14 @@
       }
 
     val new_output =
-      if (!restriction.isDefined || restriction.get.contains(new_state.command))
-        new_state.results.iterator.map(_._2).toList
+      if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
+        val rendering = Rendering(new_snapshot, PIDE.options.value)
+        rendering.output_messages(new_state)
+      }
       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
@@ -150,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"
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Dec 14 12:40:07 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.Results.empty
   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()
   }
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Dec 14 12:40:07 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()
     }
   }
 
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Dec 14 12:40:07 2012 +0100
@@ -137,6 +137,7 @@
   val hyperlink_color = color_value("hyperlink_color")
   val active_color = color_value("active_color")
   val active_hover_color = color_value("active_hover_color")
+  val active_result_color = color_value("active_result_color")
   val keyword1_color = color_value("keyword1_color")
   val keyword2_color = color_value("keyword2_color")
 
@@ -164,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)
@@ -197,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)
@@ -209,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) =>
@@ -249,31 +250,44 @@
   }
 
 
-  private val active_include = Set(Markup.SENDBACK, 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 =>
         {
-          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.defined(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 command_results(range: Text.Range): Command.Results =
+  {
+    val results =
+      snapshot.select_markup[Command.Results](range, None, command_state =>
+        { case _ => command_state.results }).map(_.info)
+    (Command.Results.empty /: results)(_ ++ _)
+  }
+
   def tooltip_message(range: Text.Range): XML.Body =
   {
     val msgs =
-      snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
-        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 ||
-              name == Markup.WARNING ||
-              name == Markup.ERROR =>
-            msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
-          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
-          if !body.isEmpty => msgs + (Document.new_id() -> msg)
-        }).toList.flatMap(_.info)
-    Pretty.separate(msgs.iterator.map(_._2).toList)
+      Command.Results.merge(
+        snapshot.cumulate_markup[Command.Results](range, Command.Results.empty,
+          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 ||
+                name == Markup.WARNING ||
+                name == Markup.ERROR =>
+              msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
+            case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
+            if !body.isEmpty => msgs + (Document.new_id() -> msg)
+          }).map(_.info))
+    Pretty.separate(msgs.entries.map(_._2).toList)
   }
 
 
@@ -307,7 +321,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(" ")
@@ -334,7 +348,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 {
@@ -359,7 +373,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 ||
@@ -385,7 +399,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 ||
@@ -396,7 +410,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)
@@ -405,6 +419,12 @@
   }
 
 
+  def output_messages(st: Command.State): List[XML.Tree] =
+  {
+    st.results.entries.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 ++
@@ -417,7 +437,7 @@
       for {
         Text.Info(r, result) <-
           snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
-            range, (Some(Protocol.Status.init), None), Some(background1_include),
+            range, (Some(Protocol.Status.init), None), Some(background1_include), command_state =>
             {
               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
               if (Protocol.command_status_markup(markup.name)) =>
@@ -426,7 +446,19 @@
                 (None, Some(bad_color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                 (None, Some(intensify_color))
-              case (_, Text.Info(_, XML.Elem(Markup(name, _), _))) if active_include(name) =>
+              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))
             })
         color <-
@@ -442,14 +474,14 @@
 
 
   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
@@ -489,7 +521,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)
diff -r 0799339fea0f -r bd145273e7c6 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Dec 14 12:40:07 2012 +0100
@@ -210,7 +210,8 @@
               if (!tip.isEmpty) {
                 val painter = text_area.getPainter
                 val y1 = y + painter.getFontMetrics.getHeight / 2
-                new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
+                val results = rendering.command_results(range)
+                new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
               }
           }
         }