more general Output.result: allow to update arbitrary properties;
clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output);

--- a/src/Pure/General/output.ML	Fri Aug 02 22:13:31 2013 +0200
+++ b/src/Pure/General/output.ML	Fri Aug 02 22:17:53 2013 +0200
@@ -35,7 +35,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 result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
     val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
   end
   val urgent_message: string -> unit
@@ -44,7 +44,7 @@
   val prompt: string -> unit
   val status: string -> unit
   val report: string -> unit
-  val result: serial * string -> unit
+  val result: Properties.T -> string -> unit
   val protocol_message: Properties.T -> string -> unit
   val try_protocol_message: Properties.T -> string -> unit
 end;
@@ -102,7 +102,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 result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
   val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
     Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
 end;
@@ -116,7 +116,7 @@
 fun prompt s = ! Internal.prompt_fn (output s);
 fun status s = ! Internal.status_fn (output s);
 fun report s = ! Internal.report_fn (output s);
-fun result (i, s) = ! Internal.result_fn (i, output s);
+fun result props s = ! Internal.result_fn props (output s);
 fun protocol_message props s = ! Internal.protocol_message_fn props (output s);
 fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
 

--- a/src/Pure/PIDE/markup.ML	Fri Aug 02 22:13:31 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Aug 02 22:17:53 2013 +0200
@@ -19,6 +19,7 @@
   val nameN: string
   val name: string -> T -> T
   val kindN: string
+  val instanceN: string
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val get_entity_kind: T -> string option
@@ -118,6 +119,7 @@
   val finishedN: string val finished: T
   val failedN: string val failed: T
   val serialN: string
+  val serial_properties: int -> Properties.T
   val exec_idN: string
   val initN: string
   val statusN: string
@@ -222,6 +224,8 @@
 
 val kindN = "kind";
 
+val instanceN = "instance";
+
 
 (* formal entities *)
 
@@ -423,6 +427,8 @@
 (* messages *)
 
 val serialN = "serial";
+fun serial_properties i = [(serialN, print_int i)];
+
 val exec_idN = "exec_id";
 
 val initN = "init";

--- a/src/Pure/PIDE/markup.scala	Fri Aug 02 22:13:31 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Aug 02 22:17:53 2013 +0200
@@ -18,6 +18,9 @@
   val KIND = "kind"
   val Kind = new Properties.String(KIND)
 
+  val INSTANCE = "instance"
+  val Instance = new Properties.String(INSTANCE)
+
 
   /* basic markup */
 

--- a/src/Pure/System/isabelle_process.ML	Fri Aug 02 22:13:31 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Aug 02 22:17:53 2013 +0200
@@ -93,6 +93,8 @@
 
 (* output channels *)
 
+val serial_props = Markup.serial_properties o serial;
+
 fun init_channels channel =
   let
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
@@ -103,21 +105,22 @@
     fun message name props body =
       Message_Channel.send msg_channel (Message_Channel.message name props body);
 
-    fun standard_message opt_serial name body =
+    fun standard_message props name body =
       if body = "" then ()
       else
         message name
-          ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
-            (Position.properties_of (Position.thread_data ()))) body;
+          (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
   in
-    Output.Internal.status_fn := standard_message NONE Markup.statusN;
-    Output.Internal.report_fn := standard_message NONE Markup.reportN;
-    Output.Internal.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
-    Output.Internal.writeln_fn := (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
+    Output.Internal.status_fn := standard_message [] Markup.statusN;
+    Output.Internal.report_fn := standard_message [] Markup.reportN;
+    Output.Internal.result_fn :=
+      (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
+    Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
     Output.Internal.tracing_fn :=
-      (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
-    Output.Internal.warning_fn := (fn s => standard_message (SOME (serial ())) Markup.warningN s);
-    Output.Internal.error_fn := (fn (i, s) => standard_message (SOME i) Markup.errorN s);
+      (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
+    Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
+    Output.Internal.error_fn :=
+      (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
     Output.Internal.protocol_message_fn := message Markup.protocolN;
     Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
     Output.Internal.prompt_fn := ignore;

--- a/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:13:31 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:17:53 2013 +0200
@@ -640,12 +640,15 @@
 
 (** print function **)
 
-val _ = Command.print_function "find_theorems"
+val find_theoremsN = "find_theorems";
+
+val _ = Command.print_function find_theoremsN
   (fn {args, ...} =>
-    if null args then NONE
-    else
+    (case args of
+      [instance, query] =>
       SOME {delay = NONE, pri = 0, persistent = false,
         print_fn = fn _ => fn st =>
-          writeln (cat_lines ("find_theorems" :: args))});
+          Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] query}
+    | _ => NONE));
 
 end;

--- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 22:13:31 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 22:17:53 2013 +0200
@@ -28,16 +28,15 @@
 
   /* component state -- owned by Swing thread */
 
-  private val identification = Document_ID.make().toString
+  private val FIND_THEOREMS = "find_theorems"
+  private val instance = Document_ID.make().toString
 
   private var zoom_factor = 100
+  private var current_location: Option[Command] = None
+  private var current_query: String = ""
   private var current_snapshot = Document.State.init.snapshot()
   private var current_state = Command.empty.init_state
   private var current_output: List[XML.Tree] = Nil
-  private var current_location: Option[Command] = None
-  private var current_query: String = ""
-
-  private val FIND_THEOREMS = "find_theorems"
 
 
   /* pretty text area */
@@ -54,9 +53,39 @@
       (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
   }
 
-  private def handle_output()
+  private def handle_update()
   {
     Swing_Thread.require()
+
+    val (new_snapshot, new_state) =
+      Document_View(view.getTextArea) match {
+        case Some(doc_view) =>
+          val snapshot = doc_view.model.snapshot()
+          if (!snapshot.is_outdated) {
+            current_location match {
+              case Some(cmd) =>
+                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
+              case None =>
+                (Document.State.init.snapshot(), Command.empty.init_state)
+            }
+          }
+          else (current_snapshot, current_state)
+        case None => (current_snapshot, current_state)
+      }
+
+    val new_output =
+      (for {
+        (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- new_state.results.entries
+        if props.contains((Markup.KIND, FIND_THEOREMS))
+        if props.contains((Markup.INSTANCE, instance))
+      } yield XML.Elem(Markup(Markup.WRITELN_MESSAGE, Nil), body)).toList
+
+    if (new_output != current_output)
+      pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
+
+    current_snapshot = new_snapshot
+    current_state = new_state
+    current_output = new_output
   }
 
   private def clear_overlay()
@@ -67,7 +96,7 @@
       command <- current_location
       buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
       model <- PIDE.document_model(buffer)
-    } model.remove_overlay(command, FIND_THEOREMS, List(identification, current_query))
+    } model.remove_overlay(command, FIND_THEOREMS, List(instance, current_query))
 
     current_location = None
     current_query = ""
@@ -85,7 +114,7 @@
           case Some(command) =>
             current_location = Some(command)
             current_query = query
-            doc_view.model.add_overlay(command, FIND_THEOREMS, List(identification, query))
+            doc_view.model.add_overlay(command, FIND_THEOREMS, List(instance, query))
           case None =>
         }
       case None =>
@@ -120,7 +149,7 @@
         case changed: Session.Commands_Changed =>
           current_location match {
             case Some(command) if changed.commands.contains(command) =>
-              Swing_Thread.later { handle_output() }
+              Swing_Thread.later { handle_update() }
             case _ =>
           }
         case bad =>