# HG changeset patch
# User wenzelm
# Date 1375476868 -7200
# Node ID 46c339daaff2bc57b57fb6a37f577f3387ef128f
# Parent  66fa0f602cc41f9488ae65e12547fe92dd555810# Parent  fb1f026c48ff9fe6a3cb23405be7fb20920678e8
merged

diff -r 66fa0f602cc4 -r 46c339daaff2 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 02 22:54:28 2013 +0200
@@ -67,9 +67,8 @@
 
 (** merges **)
 
-lemma length_merges [rule_format, simp]:
-  "\<forall>ss. size(merges f ps ss) = size ss"
-  by (induct_tac ps, auto)
+lemma length_merges [simp]: "size(merges f ps ss) = size ss"
+  by (induct ps arbitrary: ss) auto
 
 
 lemma (in Semilat) merges_preserves_type_lemma:
diff -r 66fa0f602cc4 -r 46c339daaff2 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Fri Aug 02 22:54:28 2013 +0200
@@ -137,13 +137,10 @@
 apply auto
 done
 
-lemma conf_RefTD [rule_format (no_asm)]: 
- "G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null |   
+lemma conf_RefTD [rule_format]: 
+ "G,h\<turnstile>a'::\<preceq>RefT T \<Longrightarrow> a' = Null \<or>
   (\<exists>a obj T'. a' = Addr a \<and>  h a = Some obj \<and>  obj_ty obj = T' \<and>  G\<turnstile>T'\<preceq>RefT T)"
-apply (unfold conf_def)
-apply(induct_tac "a'")
-apply(auto)
-done
+unfolding conf_def by (induct a') auto
 
 lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null"
 apply (drule conf_RefTD)
@@ -318,7 +315,7 @@
 
 lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] 
   ==> (x,(h',l))::\<preceq>(G,lT)"
-by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)
+by (fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)
 
 
 lemma conforms_upd_obj: 
diff -r 66fa0f602cc4 -r 46c339daaff2 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Fri Aug 02 22:54:28 2013 +0200
@@ -105,10 +105,7 @@
 
 lemma raise_if_Some2 [simp]: 
   "raise_if c z (if x = None then Some y else x) \<noteq> None"
-apply (unfold raise_if_def)
-apply(induct_tac "x")
-apply auto
-done
+unfolding raise_if_def by (induct x) auto
 
 lemma raise_if_SomeD [rule_format (no_asm)]: 
   "raise_if c x y = Some z \<longrightarrow> c \<and>  Some z = Some (Addr (XcptRef x)) |  y = Some z"
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/General/output.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -25,7 +25,7 @@
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
   exception Protocol_Message of Properties.T
-  structure Private_Hooks:
+  structure Internal:
   sig
     val writeln_fn: (output -> unit) Unsynchronized.ref
     val urgent_message_fn: (output -> unit) Unsynchronized.ref
@@ -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;
@@ -92,7 +92,7 @@
 
 exception Protocol_Message of Properties.T;
 
-structure Private_Hooks =
+structure Internal =
 struct
   val writeln_fn = Unsynchronized.ref physical_writeln;
   val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
@@ -102,22 +102,22 @@
   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;
 
-fun writeln s = ! Private_Hooks.writeln_fn (output s);
-fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
-fun tracing s = ! Private_Hooks.tracing_fn (output s);
-fun warning s = ! Private_Hooks.warning_fn (output s);
-fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
+fun writeln s = ! Internal.writeln_fn (output s);
+fun urgent_message s = ! Internal.urgent_message_fn (output s);
+fun tracing s = ! Internal.tracing_fn (output s);
+fun warning s = ! Internal.warning_fn (output s);
+fun error_msg' (i, s) = ! Internal.error_fn (i, output s);
 fun error_msg s = error_msg' (serial (), s);
-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);
+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 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 _ => ();
 
 end;
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -14,10 +14,11 @@
   val eval_result_state: eval -> Toplevel.state
   val eval: (unit -> theory) -> Token.T list -> eval -> eval
   type print
-  val print: bool -> string -> eval -> print list -> print list option
+  val print: bool -> (string * string list) list -> string ->
+    eval -> print list -> print list option
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   val print_function: string ->
-    ({command_name: string} ->
+    ({command_name: string, args: string list} ->
       {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
   val no_print_function: string -> unit
   type exec = eval * print list
@@ -195,13 +196,13 @@
 (* print *)
 
 datatype print = Print of
- {name: string, delay: Time.time option, pri: int, persistent: bool,
+ {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
   exec_id: Document_ID.exec, print_process: unit memo};
 
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 type print_function =
-  {command_name: string} ->
+  {command_name: string, args: string list} ->
     {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
 
 local
@@ -221,11 +222,15 @@
 
 fun print_persistent (Print {persistent, ...}) = persistent;
 
+val overlay_ord = prod_ord string_ord (list_ord string_ord);
+
 in
 
-fun print command_visible command_name eval old_prints =
+fun print command_visible command_overlays command_name eval old_prints =
   let
-    fun new_print (name, get_pr) =
+    val print_functions = Synchronized.value print_functions;
+
+    fun new_print name args get_pr =
       let
         fun make_print strict {delay, pri, persistent, print_fn} =
           let
@@ -240,11 +245,12 @@
               end;
           in
            Print {
-             name = name, delay = delay, pri = pri, persistent = persistent,
+             name = name, args = args, delay = delay, pri = pri, persistent = persistent,
              exec_id = exec_id, print_process = memo exec_id process}
           end;
+        val params = {command_name = command_name, args = args};
       in
-        (case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of
+        (case Exn.capture (Runtime.controlled_execution get_pr) params of
           Exn.Res NONE => NONE
         | Exn.Res (SOME pr) => SOME (make_print false pr)
         | Exn.Exn exn =>
@@ -252,12 +258,19 @@
               {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
       end;
 
+    fun get_print (a, b) =
+      (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
+        NONE =>
+          (case AList.lookup (op =) print_functions a of
+            NONE => NONE
+          | SOME get_pr => new_print a b get_pr)
+      | some => some);
+
     val new_prints =
       if command_visible then
-        rev (Synchronized.value print_functions) |> map_filter (fn pr =>
-          (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
-            NONE => new_print pr
-          | some => some))
+        fold (fn (a, _) => cons (a, [])) print_functions command_overlays
+        |> sort_distinct overlay_ord
+        |> map_filter get_print
       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   in
     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
@@ -276,7 +289,7 @@
 
 val _ =
   print_function "print_state"
-    (fn {command_name} =>
+    (fn {command_name, ...} =>
       SOME {delay = NONE, pri = 1, persistent = true,
         print_fn = fn tr => fn st' =>
           let
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Aug 02 22:54:28 2013 +0200
@@ -14,6 +14,9 @@
 
 object Command
 {
+  type Edit = (Option[Command], Option[Command])
+
+
   /** accumulated results from prover **/
 
   /* results */
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -9,11 +9,12 @@
 sig
   val timing: bool Unsynchronized.ref
   type node_header = string * Thy_Header.header * string list
+  type overlay = Document_ID.command * string * string list
   datatype node_edit =
     Clear |    (* FIXME unused !? *)
     Edits of (Document_ID.command option * Document_ID.command option) list |
     Deps of node_header |
-    Perspective of bool * Document_ID.command list
+    Perspective of bool * Document_ID.command list * overlay list
   type edit = string * node_edit
   type state
   val init_state: state
@@ -40,12 +41,18 @@
 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
 
 type node_header = string * Thy_Header.header * string list;
-type perspective = bool * Inttab.set * Document_ID.command option;
+
+type perspective =
+ {required: bool,  (*required node*)
+  visible: Inttab.set,  (*visible commands*)
+  visible_last: Document_ID.command option,  (*last visible command*)
+  overlays: (string * string list) list Inttab.table};  (*command id -> print function with args*)
+
 structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
 
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)
-  perspective: perspective,  (*required node, visible commands, last visible command*)
+  perspective: perspective,  (*command perspective*)
   entries: Command.exec option Entries.T,  (*command entries with excecutions*)
   result: Command.eval option}  (*result of last execution*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
@@ -57,11 +64,14 @@
 fun map_node f (Node {header, perspective, entries, result}) =
   make_node (f (header, perspective, entries, result));
 
-fun make_perspective (required, command_ids) : perspective =
-  (required, Inttab.make_set command_ids, try List.last command_ids);
+fun make_perspective (required, command_ids, overlays) : perspective =
+ {required = required,
+  visible = Inttab.make_set command_ids,
+  visible_last = try List.last command_ids,
+  overlays = Inttab.make_list (map (fn (x, y, z) => (x, (y, z))) overlays)};
 
 val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
-val no_perspective = make_perspective (false, []);
+val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
 val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
@@ -86,10 +96,11 @@
 fun set_perspective args =
   map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));
 
-val required_node = #1 o get_perspective;
-val visible_command = Inttab.defined o #2 o get_perspective;
-val visible_last = #3 o get_perspective;
+val required_node = #required o get_perspective;
+val visible_command = Inttab.defined o #visible o get_perspective;
+val visible_last = #visible_last o get_perspective;
 val visible_node = is_some o visible_last
+val overlays = Inttab.lookup_list o #overlays o get_perspective;
 
 fun map_entries f =
   map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
@@ -124,11 +135,13 @@
 
 (* node edits and associated executions *)
 
+type overlay = Document_ID.command * string * string list;
+
 datatype node_edit =
   Clear |
   Edits of (Document_ID.command option * Document_ID.command option) list |
   Deps of node_header |
-  Perspective of bool * Document_ID.command list;
+  Perspective of bool * Document_ID.command list * overlay list;
 
 type edit = string * node_edit;
 
@@ -429,9 +442,10 @@
               SOME (eval, prints) =>
                 let
                   val command_visible = visible_command node command_id;
+                  val command_overlays = overlays node command_id;
                   val command_name = the_command_name state command_id;
                 in
-                  (case Command.print command_visible command_name eval prints of
+                  (case Command.print command_visible command_overlays command_name eval prints of
                     SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
                   | NONE => I)
                 end
@@ -449,15 +463,18 @@
 
 fun illegal_init _ = error "Illegal theory header after end of theory";
 
-fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
+fun new_exec state node proper_init command_id' (assign_update, command_exec, init) =
   if not proper_init andalso is_none init then NONE
   else
     let
       val (_, (eval, _)) = command_exec;
+
+      val command_visible = visible_command node command_id';
+      val command_overlays = overlays node command_id';
       val (command_name, span) = the_command state command_id' ||> Lazy.force;
 
       val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
-      val prints' = perhaps (Command.print command_visible command_name eval') [];
+      val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
       val exec' = (eval', prints');
 
       val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
@@ -512,7 +529,7 @@
                         iterate_entries_after common
                           (fn ((prev, id), _) => fn res =>
                             if not node_required andalso prev = visible_last node then NONE
-                            else new_exec state proper_init (visible_command node id) id res) node;
+                            else new_exec state node proper_init id res) node;
 
                     val assigned_execs =
                       (node0, updated_execs) |-> iterate_entries_after common
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 02 22:54:28 2013 +0200
@@ -15,11 +15,28 @@
 {
   /** document structure **/
 
+  /* overlays -- print functions with arguments */
+
+  type Overlay = (Command, String, List[String])
+
+  object Overlays
+  {
+    val empty = new Overlays(Set.empty)
+  }
+
+  final class Overlays private(rep: Set[Overlay])
+  {
+    def + (o: Overlay) = new Overlays(rep + o)
+    def - (o: Overlay) = new Overlays(rep - o)
+    def dest: List[Overlay] = rep.toList
+  }
+
+
   /* individual nodes */
 
   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
-  type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
+  type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
   object Node
   {
@@ -66,8 +83,9 @@
     case class Clear[A, B]() extends Edit[A, B]
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     case class Deps[A, B](header: Header) extends Edit[A, B]
-    case class Perspective[A, B](required: Boolean, perspective: B) extends Edit[A, B]
+    case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
+    type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
@@ -87,7 +105,8 @@
 
   final class Node private(
     val header: Node.Header = Node.bad_header("Bad theory header"),
-    val perspective: (Boolean, Command.Perspective) = (false, Command.Perspective.empty),
+    val perspective: Node.Perspective_Command =
+      Node.Perspective(false, Command.Perspective.empty, Overlays.empty),
     val commands: Linear_Set[Command] = Linear_Set.empty)
   {
     def clear: Node = new Node(header = header)
@@ -95,11 +114,13 @@
     def update_header(new_header: Node.Header): Node =
       new Node(new_header, perspective, commands)
 
-    def update_perspective(new_perspective: (Boolean, Command.Perspective)): Node =
+    def update_perspective(new_perspective: Node.Perspective_Command): Node =
       new Node(header, new_perspective, commands)
 
-    def same_perspective(other: (Boolean, Command.Perspective)): Boolean =
-      perspective._1 == other._1 && (perspective._2 same other._2)
+    def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
+      perspective.required == other_perspective.required &&
+      perspective.visible.same(other_perspective.visible) &&
+      perspective.overlays == other_perspective.overlays
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       new Node(header, perspective, new_commands)
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Aug 02 22:54:28 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";
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Aug 02 22:54:28 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 */
 
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -56,7 +56,9 @@
                       val imports' = map (rpair Position.none) imports;
                       val header = Thy_Header.make (name, Position.none) imports' keywords;
                     in Document.Deps (master, header, errors) end,
-                  fn (a :: b, []) => Document.Perspective (bool_atom a, map int_atom b)]))
+                  fn (a :: b, c) =>
+                    Document.Perspective (bool_atom a, map int_atom b,
+                      list (triple int string (list string)) c)]))
             end;
 
         val (removed, assign_update, state') = Document.update old_id new_id edits state;
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Aug 02 22:54:28 2013 +0200
@@ -326,7 +326,7 @@
     { import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
       def encode_edit(name: Document.Node.Name)
-          : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
+          : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
         variant(List(
           { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
@@ -340,8 +340,9 @@
                     option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
                   list(Encode.string)))))(
                 (dir, (name.theory, (imports, (keywords, header.errors)))))) },
-          { case Document.Node.Perspective(a, b) =>
-              (bool_atom(a) :: b.commands.map(c => long_atom(c.id)), Nil) }))
+          { case Document.Node.Perspective(a, b, c) =>
+              (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
+                list(triple(id, Encode.string, list(Encode.string)))(c.dest)) }))
       def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
       {
         val (name, edit) = node_edit
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Aug 02 22:54:28 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,27 +105,25 @@
     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.Private_Hooks.status_fn := standard_message NONE Markup.statusN;
-    Output.Private_Hooks.report_fn := standard_message NONE Markup.reportN;
-    Output.Private_Hooks.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
-    Output.Private_Hooks.writeln_fn :=
-      (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
-    Output.Private_Hooks.tracing_fn :=
-      (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
-    Output.Private_Hooks.warning_fn :=
-      (fn s => standard_message (SOME (serial ())) Markup.warningN s);
-    Output.Private_Hooks.error_fn :=
-      (fn (i, s) => standard_message (SOME i) Markup.errorN s);
-    Output.Private_Hooks.protocol_message_fn := message Markup.protocolN;
-    Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
-    Output.Private_Hooks.prompt_fn := ignore;
+    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 (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;
     message Markup.initN [] (Session.welcome ());
     msg_channel
   end;
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/System/isar.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -156,7 +156,7 @@
 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
   if do_init then init () else ();
-  Output.Private_Hooks.protocol_message_fn := protocol_message;
+  Output.Internal.protocol_message_fn := protocol_message;
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
 
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 02 22:54:28 2013 +0200
@@ -293,7 +293,7 @@
   /* main */
 
   def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
-    : List[(Option[Command], Option[Command])] =
+    : List[Command.Edit] =
   {
     val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
     val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
@@ -311,17 +311,18 @@
       case (name, Document.Node.Edits(text_edits)) =>
         val commands0 = node.commands
         val commands1 = edit_text(text_edits, commands0)
-        val commands2 = recover_spans(syntax, name, node.perspective._2, commands1)
+        val commands2 = recover_spans(syntax, name, node.perspective.visible, commands1)
         node.update_commands(commands2)
 
       case (_, Document.Node.Deps(_)) => node
 
-      case (name, Document.Node.Perspective(required, text_perspective)) =>
-        val perspective = (required, command_perspective(node, text_perspective))
+      case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
+        val perspective: Document.Node.Perspective_Command =
+          Document.Node.Perspective(required, command_perspective(node, text_perspective), overlays)
         if (node.same_perspective(perspective)) node
         else
           node.update_perspective(perspective).update_commands(
-            consolidate_spans(syntax, reparse_limit, name, perspective._2, node.commands))
+            consolidate_spans(syntax, reparse_limit, name, perspective.visible, node.commands))
     }
   }
 
@@ -354,8 +355,7 @@
         val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
 
         if (!(node.same_perspective(node2.perspective)))
-          doc_edits +=
-            (name -> Document.Node.Perspective(node2.perspective._1, node2.perspective._2))
+          doc_edits += (name -> node2.perspective)
 
         doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
 
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/Tools/build.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -164,7 +164,7 @@
         theories |>
           (List.app (use_theories_condition last_timing)
             |> session_timing name verbose
-            |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
+            |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message
             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
             |> Exn.capture);
       val res2 = Exn.capture Session.finish ();
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -21,7 +21,7 @@
   }
 
   val read_criterion: Proof.context -> string criterion -> term criterion
-  val query_parser: (bool * string criterion) list parser
+  val parse_query: string -> (bool * string criterion) list
 
   val xml_of_query: term query -> XML.tree
   val query_of_xml: XML.tree -> term query
@@ -496,7 +496,7 @@
 end;
 
 
-(* print_theorems *)
+(* pretty_theorems *)
 
 fun all_facts_of ctxt =
   let
@@ -572,11 +572,12 @@
 
 fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
 
-fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
+fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
-    val (foundo, theorems) = find
-      {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
+    val (foundo, theorems) =
+      filter_theorems ctxt (map Internal (all_facts_of ctxt))
+        {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
     val returned = length theorems;
 
     val tally_msg =
@@ -594,10 +595,13 @@
      else
       [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
         grouped 10 Par_List.map (pretty_theorem ctxt) theorems)
-  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
+  end |> Pretty.fbreaks |> curry Pretty.blk 0;
 
-fun print_theorems ctxt =
-  gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
+fun pretty_theorems_cmd state opt_lim rem_dups spec =
+  let
+    val ctxt = Toplevel.context_of state;
+    val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
+  in pretty_theorems ctxt opt_goal opt_lim rem_dups spec end;
 
 
 
@@ -619,21 +623,47 @@
     (Parse.$$$ "(" |--
       Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
         --| Parse.$$$ ")")) (NONE, true);
+
+val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
+
 in
 
-val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
+(* FIXME proper wrapper for parser combinator *)
+fun parse_query str =
+  (str ^ ";")
+  |> Outer_Syntax.scan Position.start
+  |> filter Token.is_proper
+  |> Scan.error query_parser
+  |> fst;
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "find_theorems"}
     "find theorems meeting specified criteria"
-    (options -- query_parser
-      >> (fn ((opt_lim, rem_dups), spec) =>
-        Toplevel.keep (fn state =>
-          let
-            val ctxt = Toplevel.context_of state;
-            val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
-          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
+    (options -- query_parser >> (fn ((opt_lim, rem_dups), spec) =>
+      Toplevel.keep (fn state =>
+        Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
 
 end;
 
+
+
+(** print function **)
+
+val find_theoremsN = "find_theorems";
+
+val _ = Command.print_function find_theoremsN
+  (fn {args, ...} =>
+    (case args of
+      [instance, query] =>
+      SOME {delay = NONE, pri = 0, persistent = false,
+        print_fn = fn _ => fn state =>
+          let
+            val msg =
+              Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query))
+                handle exn =>
+                  if Exn.is_interrupt exn then reraise exn
+                  else ML_Compiler.exn_message exn;  (* FIXME error markup!? *)
+          in Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] msg end}
+    | _ => NONE));
+
 end;
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -261,14 +261,14 @@
   | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
- (Output.Private_Hooks.writeln_fn := message "" "" "";
-  Output.Private_Hooks.status_fn := (fn _ => ());
-  Output.Private_Hooks.report_fn := (fn _ => ());
-  Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
-  Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
-  Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
-  Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
-  Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
+ (Output.Internal.writeln_fn := message "" "" "";
+  Output.Internal.status_fn := (fn _ => ());
+  Output.Internal.report_fn := (fn _ => ());
+  Output.Internal.urgent_message_fn := message (special "I") (special "J") "";
+  Output.Internal.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+  Output.Internal.warning_fn := message (special "K") (special "L") "### ";
+  Output.Internal.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
+  Output.Internal.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
 
 
 (* notification *)
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -16,12 +16,7 @@
     val args = Symtab.lookup arg_data;
 
     val query_str = the_default "" (args "query");
-    fun get_query () =
-      (query_str ^ ";")
-      |> Outer_Syntax.scan Position.start
-      |> filter Token.is_proper
-      |> Scan.error Find_Theorems.query_parser
-      |> fst;
+    fun get_query () = Find_Theorems.parse_query query_str;
 
     val limit = case args "limit" of
         NONE => default_limit
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 02 22:54:28 2013 +0200
@@ -13,6 +13,7 @@
   "src/document_model.scala"
   "src/document_view.scala"
   "src/documentation_dockable.scala"
+  "src/find_dockable.scala"
   "src/fold_handling.scala"
   "src/graphview_dockable.scala"
   "src/html_panel.scala"
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Fri Aug 02 22:54:28 2013 +0200
@@ -31,6 +31,7 @@
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
 plugin.isabelle.jedit.Plugin.menu= \
   isabelle.documentation-panel \
+  isabelle.find-panel \
   isabelle.monitor-panel \
   isabelle.output-panel \
   isabelle.protocol-panel \
@@ -41,6 +42,7 @@
   isabelle.theories-panel \
   isabelle.timing-panel
 isabelle.documentation-panel.label=Documentation panel
+isabelle.find-panel.label=Find panel
 isabelle.monitor-panel.label=Monitor panel
 isabelle.output-panel.label=Output panel
 isabelle.protocol-panel.label=Protocol panel
@@ -52,6 +54,7 @@
 isabelle.timing-panel.label=Timing panel
 
 #dockables
+isabelle-find.title=Find
 isabelle-graphview.title=Graphview
 isabelle-info.title=Info
 isabelle-monitor.title=Monitor
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Fri Aug 02 22:54:28 2013 +0200
@@ -27,6 +27,11 @@
 			wm.addDockableWindow("isabelle-readme");
 		</CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.find-panel">
+		<CODE>
+			wm.addDockableWindow("isabelle-find");
+		</CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.output-panel">
 		<CODE>
 			wm.addDockableWindow("isabelle-output");
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Tools/jEdit/src/dockables.xml
--- a/src/Tools/jEdit/src/dockables.xml	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/dockables.xml	Fri Aug 02 22:54:28 2013 +0200
@@ -20,6 +20,9 @@
 	<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
 		new isabelle.jedit.Output_Dockable(view, position);
 	</DOCKABLE>
+	<DOCKABLE NAME="isabelle-find" MOVABLE="TRUE">
+		new isabelle.jedit.Find_Dockable(view, position);
+	</DOCKABLE>
 	<DOCKABLE NAME="isabelle-info" MOVABLE="TRUE">
 		new isabelle.jedit.Info_Dockable(view, position);
 	</DOCKABLE>
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Aug 02 22:54:28 2013 +0200
@@ -77,8 +77,28 @@
   }
 
 
+  /* overlays */
+
+  private var overlays = Document.Overlays.empty
+
+  def add_overlay(command: Command, name: String, args: List[String])
+  {
+    Swing_Thread.required()
+    overlays += ((command, name, args))
+    PIDE.flush_buffers()
+  }
+
+  def remove_overlay(command: Command, name: String, args: List[String])
+  {
+    Swing_Thread.required()
+    overlays -= ((command, name, args))
+    PIDE.flush_buffers()
+  }
+
+
   /* perspective */
 
+  // owned by Swing thread
   private var _node_required = false
   def node_required: Boolean = _node_required
   def node_required_=(b: Boolean)
@@ -91,21 +111,21 @@
     }
   }
 
+  val empty_perspective: Document.Node.Perspective_Text =
+    Document.Node.Perspective(false, Text.Perspective.empty, Document.Overlays.empty)
+
   def node_perspective(): Document.Node.Perspective_Text =
   {
     Swing_Thread.require()
 
-    val perspective =
-      if (Isabelle.continuous_checking) {
-        (node_required, Text.Perspective(
-          for {
-            doc_view <- PIDE.document_views(buffer)
-            range <- doc_view.perspective().ranges
-          } yield range))
-      }
-      else (false, Text.Perspective.empty)
-
-    Document.Node.Perspective(perspective._1, perspective._2)
+    if (Isabelle.continuous_checking) {
+      Document.Node.Perspective(node_required, Text.Perspective(
+        for {
+          doc_view <- PIDE.document_views(buffer)
+          range <- doc_view.perspective().ranges
+        } yield range), overlays)
+    }
+    else empty_perspective
   }
 
 
@@ -143,8 +163,7 @@
   private object pending_edits  // owned by Swing thread
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
-    private var last_perspective: Document.Node.Perspective_Text =
-      Document.Node.Perspective(node_required, Text.Perspective.empty)
+    private var last_perspective = empty_perspective
 
     def snapshot(): List[Text.Edit] = pending.toList
 
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Tools/jEdit/src/find_dockable.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 22:54:28 2013 +0200
@@ -0,0 +1,217 @@
+/*  Title:      Tools/jEdit/src/find_dockable.scala
+    Author:     Makarius
+
+Dockable window for "find" dialog.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+
+import scala.swing.{FlowPanel, Button, Component}
+import scala.swing.event.ButtonClicked
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.HistoryTextArea
+
+
+class Find_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+  Swing_Thread.require()
+
+
+  /* component state -- owned by Swing thread */
+
+  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
+
+
+  /* pretty text area */
+
+  val pretty_text_area = new Pretty_Text_Area(view)
+  set_content(pretty_text_area)
+
+
+  private def handle_resize()
+  {
+    Swing_Thread.require()
+
+    pretty_text_area.resize(Rendering.font_family(),
+      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+  }
+
+  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()
+  {
+    Swing_Thread.require()
+
+    for {
+      command <- current_location
+      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
+      model <- PIDE.document_model(buffer)
+    } model.remove_overlay(command, FIND_THEOREMS, List(instance, current_query))
+
+    current_location = None
+    current_query = ""
+  }
+
+  private def apply_query(query: String)
+  {
+    Swing_Thread.require()
+
+    clear_overlay()
+    Document_View(view.getTextArea) match {
+      case Some(doc_view) =>
+        val snapshot = doc_view.model.snapshot()
+        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
+          case Some(command) =>
+            current_location = Some(command)
+            current_query = query
+            doc_view.model.add_overlay(command, FIND_THEOREMS, List(instance, query))
+          case None =>
+        }
+      case None =>
+    }
+  }
+
+  private def locate_query()
+  {
+    Swing_Thread.require()
+
+    current_location match {
+      case Some(command) =>
+        val snapshot = PIDE.session.snapshot(command.node_name)
+        val commands = snapshot.node.commands
+        if (commands.contains(command)) {
+          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
+          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+          Hyperlink(command.node_name.node, line, column).follow(view)
+        }
+      case None =>
+    }
+  }
+
+
+  /* main actor */
+
+  private val main_actor = actor {
+    loop {
+      react {
+        case _: Session.Global_Options =>
+          Swing_Thread.later { handle_resize() }
+        case changed: Session.Commands_Changed =>
+          current_location match {
+            case Some(command) if changed.commands.contains(command) =>
+              Swing_Thread.later { handle_update() }
+            case _ =>
+          }
+        case bad =>
+          java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  override def init()
+  {
+    Swing_Thread.require()
+
+    PIDE.session.global_options += main_actor
+    PIDE.session.commands_changed += main_actor
+    handle_resize()
+  }
+
+  override def exit()
+  {
+    Swing_Thread.require()
+
+    PIDE.session.global_options -= main_actor
+    PIDE.session.commands_changed -= main_actor
+    delay_resize.revoke()
+  }
+
+
+  /* resize */
+
+  private val delay_resize =
+    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+  addComponentListener(new ComponentAdapter {
+    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+  })
+
+
+  /* controls */
+
+  private val query = new HistoryTextArea("isabelle-find-theorems") {
+    { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
+    setColumns(25)
+    setRows(1)
+  }
+
+  private val query_wrapped = Component.wrap(query)
+
+  private val find = new Button("Find") {
+    tooltip = "Find theorems meeting specified criteria"
+    reactions += { case ButtonClicked(_) => apply_query(query.getText) }
+  }
+
+  private val locate = new Button("Locate") {
+    tooltip = "Locate context of current query within source text"
+    reactions += { case ButtonClicked(_) => locate_query() }
+  }
+
+  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
+    tooltip = "Zoom factor for output font size"
+  }
+
+  private val controls =
+    new FlowPanel(FlowPanel.Alignment.Right)(query_wrapped, find, locate, zoom)
+  add(controls.peer, BorderLayout.NORTH)
+}
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Aug 02 22:54:28 2013 +0200
@@ -135,30 +135,31 @@
 
   /* controls */
 
-  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
-  zoom.tooltip = "Zoom factor for basic font size"
+  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
+    tooltip = "Zoom factor for output font size"
+  }
 
   private val auto_update = new CheckBox("Auto update") {
+    tooltip = "Indicate automatic update following cursor movement"
     reactions += {
       case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
+    selected = do_update
   }
-  auto_update.selected = do_update
-  auto_update.tooltip = "Indicate automatic update following cursor movement"
 
   private val update = new Button("Update") {
+    tooltip = "Update display according to the command at cursor position"
     reactions += { case ButtonClicked(_) => handle_update(true, None) }
   }
-  update.tooltip = "Update display according to the command at cursor position"
 
   private val detach = new Button("Detach") {
+    tooltip = "Detach window with static copy of current output"
     reactions += {
       case ButtonClicked(_) =>
         Info_Dockable(view, current_snapshot,
           current_state.results, Pretty.separate(current_output))
     }
   }
-  detach.tooltip = "Detach window with static copy of current output"
 
-  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, auto_update, update, detach)
+  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(auto_update, update, detach, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }
diff -r 66fa0f602cc4 -r 46c339daaff2 src/Tools/try.ML
--- a/src/Tools/try.ML	Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/try.ML	Fri Aug 02 22:54:28 2013 +0200
@@ -117,7 +117,7 @@
 
 fun print_function ((name, (weight, auto, tool)): tool) =
   Command.print_function name
-    (fn {command_name} =>
+    (fn {command_name, ...} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
         SOME
          {delay = SOME (seconds (Options.default_real @{option auto_time_start})),