# HG changeset patch
# User wenzelm
# Date 1399304935 -7200
# Node ID 1902d7c260174b6fccd175e183934ef0bfe5c2e1
# Parent  bc50d5e04e902add478c7fa5c25133ddb37807cb# Parent  6e26ae897badccf581b32aed33269d9e578a4892
merged

diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Mon May 05 17:48:55 2014 +0200
@@ -16,12 +16,6 @@
 
 object Simple_Thread
 {
-  /* pending interrupts */
-
-  def interrupted_exception(): Unit =
-    if (Thread.interrupted()) throw Exn.Interrupt()
-
-
   /* plain thread */
 
   def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/General/exn.scala	Mon May 05 17:48:55 2014 +0200
@@ -45,6 +45,22 @@
     def apply(): Throwable = new InterruptedException
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
+    def expose() { if (Thread.interrupted()) throw apply() }
+    def impose() { Thread.currentThread.interrupt }
+
+    def postpone[A](body: => A): Option[A] =
+    {
+      val interrupted = Thread.interrupted
+      val result = capture { body }
+      if (interrupted) impose()
+      result match {
+        case Res(x) => Some(x)
+        case Exn(e) =>
+          if (is_interrupt(e)) { impose(); None }
+          else throw e
+      }
+    }
+
     val return_code = 130
   }
 
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon May 05 17:48:55 2014 +0200
@@ -35,7 +35,7 @@
   val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   val diag_state: Proof.context -> Toplevel.state
   val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
-  val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
+  val pretty_theorems: bool -> Toplevel.state -> Pretty.T
   val thy_deps: Toplevel.transition -> Toplevel.transition
   val locale_deps: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
@@ -258,20 +258,19 @@
     (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
 
 
-(* print theorems *)
-
-fun print_theorems_proof verbose =
-  Toplevel.keep (fn st =>
-    Proof_Context.print_local_facts (Proof.context_of (Toplevel.proof_of st)) verbose);
+(* theorems of theory or proof context *)
 
-fun print_theorems_theory verbose = Toplevel.keep (fn state =>
-  Toplevel.theory_of state |>
-  (case Toplevel.previous_context_of state of
-    SOME prev => Proof_Display.print_theorems_diff verbose (Proof_Context.theory_of prev)
-  | NONE => Proof_Display.print_theorems verbose));
-
-fun print_theorems verbose =
-  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof verbose;
+fun pretty_theorems verbose st =
+  if Toplevel.is_proof st then
+    Pretty.chunks (Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose)
+  else
+    let
+      val thy = Toplevel.theory_of st;
+      val prev_thys =
+        (case Toplevel.previous_context_of st of
+          SOME prev => [Proof_Context.theory_of prev]
+        | NONE => Theory.parents_of thy);
+    in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
 
 
 (* display dependencies *)
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon May 05 17:48:55 2014 +0200
@@ -673,32 +673,36 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "qed"} "conclude proof"
-    (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m)));
+    (Scan.option Method.parse >> (fn m =>
+     (Option.map Method.report m;
+      Toplevel.print o Isar_Cmd.qed m)));
 
 val _ =
   Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
     (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
-      (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2))));
+     (Method.report m1;
+      Option.map Method.report m2;
+      Toplevel.print o Isar_Cmd.terminal_proof (m1, m2))));
 
 val _ =
   Outer_Syntax.command @{command_spec ".."} "default proof"
-    (Scan.succeed Isar_Cmd.default_proof);
+    (Scan.succeed (Toplevel.print o Isar_Cmd.default_proof));
 
 val _ =
   Outer_Syntax.command @{command_spec "."} "immediate proof"
-    (Scan.succeed Isar_Cmd.immediate_proof);
+    (Scan.succeed (Toplevel.print o Isar_Cmd.immediate_proof));
 
 val _ =
   Outer_Syntax.command @{command_spec "done"} "done proof"
-    (Scan.succeed Isar_Cmd.done_proof);
+    (Scan.succeed (Toplevel.print o Isar_Cmd.done_proof));
 
 val _ =
   Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
-    (Scan.succeed Isar_Cmd.skip_proof);
+    (Scan.succeed (Toplevel.print o Isar_Cmd.skip_proof));
 
 val _ =
   Outer_Syntax.command @{command_spec "oops"} "forget proof"
-    (Scan.succeed Toplevel.forget_proof);
+    (Scan.succeed (Toplevel.print o Toplevel.forget_proof));
 
 
 (* proof steps *)
@@ -742,7 +746,8 @@
       Toplevel.skip_proof (fn h => (report_back (); h))));
 
 
-(* nested commands *)
+
+(** nested commands **)
 
 val props_text =
   Scan.optional Parse.properties [] -- Parse.position Parse.string
@@ -788,7 +793,7 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
-    (Scan.succeed (Toplevel.keep Toplevel.print_state_context));
+    (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_state_context)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theory"}
@@ -817,7 +822,8 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theorems"}
     "print theorems of local theory or proof context"
-    (opt_bang >> Isar_Cmd.print_theorems);
+    (opt_bang >> (fn b =>
+      Toplevel.unknown_context o Toplevel.keep (Pretty.writeln o Isar_Cmd.pretty_theorems b)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_locales"}
@@ -905,7 +911,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
     (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of)));
+      Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_binds o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
@@ -915,7 +921,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
     (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of)));
+      Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_statement"}
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon May 05 17:48:55 2014 +0200
@@ -161,9 +161,10 @@
   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
-  val print_binds: Proof.context -> unit
+  val pretty_binds: Proof.context -> Pretty.T list
+  val pretty_local_facts: Proof.context -> bool -> Pretty.T list
   val print_local_facts: Proof.context -> bool -> unit
-  val print_cases: Proof.context -> unit
+  val pretty_cases: Proof.context -> Pretty.T list
   val debug: bool Config.T
   val verbose: bool Config.T
   val pretty_ctxt: Proof.context -> Pretty.T list
@@ -1265,8 +1266,6 @@
     else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
   end;
 
-val print_binds = Pretty.writeln_chunks o pretty_binds;
-
 
 (* local facts *)
 
@@ -1332,8 +1331,6 @@
     else [Pretty.big_list "cases:" (map pretty_case cases)]
   end;
 
-val print_cases = Pretty.writeln_chunks o pretty_cases;
-
 end;
 
 
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon May 05 17:48:55 2014 +0200
@@ -12,8 +12,8 @@
   val pp_term: theory -> term -> Pretty.T
   val pp_ctyp: ctyp -> Pretty.T
   val pp_cterm: cterm -> Pretty.T
-  val print_theorems_diff: bool -> theory -> theory -> unit
-  val print_theorems: bool -> theory -> unit
+  val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T
+  val pretty_theorems: bool -> theory -> Pretty.T
   val pretty_full_theory: bool -> theory -> Pretty.T
   val print_theory: theory -> unit
   val string_of_rule: Proof.context -> string -> thm -> string
@@ -66,11 +66,8 @@
     val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
   in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
 
-fun print_theorems_diff verbose prev_thy thy =
-  Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
-
-fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
-val print_theorems = Pretty.writeln oo pretty_theorems;
+fun pretty_theorems verbose thy =
+  pretty_theorems_diff verbose (Theory.parents_of thy) thy;
 
 fun pretty_full_theory verbose thy =
   Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon May 05 17:48:55 2014 +0200
@@ -22,7 +22,8 @@
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
   val end_theory: Position.T -> state -> theory
-  val print_state_context: state -> unit
+  val pretty_state_context: state -> Pretty.T list
+  val pretty_state: bool -> state -> Pretty.T list
   val print_state: bool -> state -> unit
   val pretty_abstract: state -> Pretty.T
   val quiet: bool Unsynchronized.ref
@@ -199,22 +200,23 @@
 
 val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
 
-fun print_state_context state =
+fun pretty_state_context state =
   (case try node_of state of
     NONE => []
   | SOME (Theory (gthy, _)) => pretty_context gthy
   | SOME (Proof (_, (_, gthy))) => pretty_context gthy
-  | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy)
-  |> Pretty.writeln_chunks;
+  | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy);
 
-fun print_state prf_only state =
+fun pretty_state prf_only state =
   (case try node_of state of
     NONE => []
   | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
   | SOME (Proof (prf, _)) =>
       Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
-  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
-  |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
+  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
+
+fun print_state prf_only =
+  pretty_state prf_only #> Pretty.markup_chunks Markup.state #> Pretty.writeln;
 
 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
 
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon May 05 17:48:55 2014 +0200
@@ -183,6 +183,8 @@
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val use_theories_result: string -> bool -> Properties.T
+  val print_operationsN: string
+  val print_operations: Properties.T
   val simp_trace_logN: string
   val simp_trace_stepN: string
   val simp_trace_recurseN: string
@@ -578,6 +580,9 @@
 fun use_theories_result id ok =
   [("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)];
 
+val print_operationsN = "print_operations";
+val print_operations = [(functionN, print_operationsN)];
+
 
 (* simplifier trace *)
 
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon May 05 17:48:55 2014 +0200
@@ -459,6 +459,8 @@
       }
   }
 
+  val PRINT_OPERATIONS = "print_operations"
+
 
   /* simplifier trace */
 
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Mon May 05 17:48:55 2014 +0200
@@ -98,6 +98,7 @@
 
   abstract class Protocol_Handler
   {
+    def start(prover: Prover): Unit = {}
     def stop(prover: Prover): Unit = {}
     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
   }
@@ -122,6 +123,8 @@
       val (handlers2, functions2) =
         try {
           val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
+          new_handler.start(prover)
+
           val new_functions =
             for ((a, f) <- new_handler.functions.toList) yield
               (a, (msg: Prover.Protocol_Output) => f(prover, msg))
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Pure.thy	Mon May 05 17:48:55 2014 +0200
@@ -108,6 +108,7 @@
 
 ML_file "ML/ml_antiquotations.ML"
 ML_file "ML/ml_thms.ML"
+ML_file "Tools/print_operation.ML"
 ML_file "Isar/isar_syn.ML"
 ML_file "Isar/calculation.ML"
 ML_file "Tools/rail.ML"
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/System/interrupt.scala
--- a/src/Pure/System/interrupt.scala	Mon May 05 10:03:43 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-/*  Title:      Pure/System/interrupt.scala
-    Author:     Makarius
-
-Support for POSIX interrupts (bypassed on Windows).
-*/
-
-package isabelle
-
-
-import sun.misc.{Signal, SignalHandler}
-
-
-object Interrupt
-{
-  def handler[A](h: => Unit)(e: => A): A =
-  {
-    val SIGINT = new Signal("INT")
-    val new_handler = new SignalHandler { def handle(s: Signal) { h } }
-    val old_handler = Signal.handle(SIGINT, new_handler)
-    try { e } finally { Signal.handle(SIGINT, old_handler) }
-  }
-
-  def exception[A](e: => A): A =
-  {
-    val thread = Thread.currentThread
-    handler { thread.interrupt } { e }
-  }
-}
-
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon May 05 17:48:55 2014 +0200
@@ -327,13 +327,7 @@
       execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid).waitFor
 
     private def kill(signal: String): Boolean =
-    {
-      try {
-        kill_cmd(signal)
-        kill_cmd("0") == 0
-      }
-      catch { case Exn.Interrupt() => true }
-    }
+      Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
 
     private def multi_kill(signal: String): Boolean =
     {
@@ -341,8 +335,10 @@
       var count = 10
       while (running && count > 0) {
         if (kill(signal)) {
-          try { Thread.sleep(100) } catch { case Exn.Interrupt() => }
-          count -= 1
+          Exn.Interrupt.postpone {
+            Thread.sleep(100)
+            count -= 1
+          }
         }
         else running = false
       }
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/System/posix_interrupt.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/posix_interrupt.scala	Mon May 05 17:48:55 2014 +0200
@@ -0,0 +1,29 @@
+/*  Title:      Pure/System/interrupt.scala
+    Author:     Makarius
+
+Support for POSIX interrupts (bypassed on Windows).
+*/
+
+package isabelle
+
+
+import sun.misc.{Signal, SignalHandler}
+
+
+object POSIX_Interrupt
+{
+  def handler[A](h: => Unit)(e: => A): A =
+  {
+    val SIGINT = new Signal("INT")
+    val new_handler = new SignalHandler { def handle(s: Signal) { h } }
+    val old_handler = Signal.handle(SIGINT, new_handler)
+    try { e } finally { Signal.handle(SIGINT, old_handler) }
+  }
+
+  def exception[A](e: => A): A =
+  {
+    val thread = Thread.currentThread
+    handler { thread.interrupt } { e }
+  }
+}
+
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Tools/build.scala	Mon May 05 17:48:55 2014 +0200
@@ -37,7 +37,7 @@
       if (verbose) echo(session + ": theory " + theory)
 
     @volatile private var is_stopped = false
-    def interrupt_handler[A](e: => A): A = Interrupt.handler { is_stopped = true } { e }
+    def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
     override def stopped: Boolean =
     {
       if (Thread.interrupted) is_stopped = true
@@ -814,7 +814,7 @@
     def sleep()
     {
       try { Thread.sleep(500) }
-      catch { case Exn.Interrupt() => Thread.currentThread.interrupt }
+      catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
     }
 
     @tailrec def loop(
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Tools/print_operation.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/print_operation.ML	Mon May 05 17:48:55 2014 +0200
@@ -0,0 +1,84 @@
+(*  Title:      Pure/Tools/print_operation.ML
+    Author:     Makarius
+
+Print operations as asynchronous query.
+*)
+
+
+signature PRINT_OPERATION =
+sig
+  val register: string -> string -> (Toplevel.state -> string) -> unit
+end;
+
+structure Print_Operation: PRINT_OPERATION =
+struct
+
+(* maintain print operations *)
+
+local
+
+val print_operations =
+  Synchronized.var "print_operations"
+    ([]: (string * (string * (Toplevel.state -> string))) list);
+
+fun report () =
+  Output.try_protocol_message Markup.print_operations
+    let
+      val yxml =
+        Synchronized.value print_operations
+        |> map (fn (x, (y, _)) => (x, y)) |> rev
+        |> let open XML.Encode in list (pair string string) end
+        |> YXML.string_of_body;
+    in [yxml] end;
+
+val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
+
+val _ = Session.protocol_handler "isabelle.Print_Operation$Handler";
+
+in
+
+fun register name description pr =
+ (Synchronized.change print_operations (fn tab =>
+   (if not (AList.defined (op =) tab name) then ()
+    else warning ("Redefining print operation: " ^ quote name);
+    AList.update (op =) (name, (description, pr)) tab));
+  report ());
+
+val _ =
+  Query_Operation.register "print_operation" (fn {state, args, output_result} =>
+    let
+      val [name] = args;
+      val pr =
+        (case AList.lookup (op =) (Synchronized.value print_operations) name of
+          SOME (_, pr) => pr
+        | NONE => error ("Unknown print operation: " ^ quote name));
+      val result = pr state handle Toplevel.UNDEF => error "Unknown context";
+    in output_result result end);
+
+end;
+
+
+(* common print operations *)
+
+val _ =
+  register "context" "main context"
+    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state_context);
+
+val _ =
+  register "cases" "cases of proof context"
+    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of);
+
+val _ =
+  register "terms" "term bindings of proof context"
+    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_binds o Toplevel.context_of);
+
+val _ =
+  register "theorems" "theorems of local theory or proof context"
+    (Pretty.string_of o Isar_Cmd.pretty_theorems false);
+
+val _ =
+  register "state" "proof state"
+    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state true);
+
+end;
+
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/Tools/print_operation.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/print_operation.scala	Mon May 05 17:48:55 2014 +0200
@@ -0,0 +1,43 @@
+/*  Title:      Pure/System/print_operation.scala
+    Author:     Makarius
+
+Print operations as asynchronous query.
+*/
+
+package isabelle
+
+
+object Print_Operation
+{
+  def print_operations(session: Session): List[(String, String)] =
+    session.protocol_handler("isabelle.Print_Operation$Handler") match {
+      case Some(handler: Handler) => handler.get
+      case _ => Nil
+    }
+
+
+  /* protocol handler */
+
+  class Handler extends Session.Protocol_Handler
+  {
+    private val print_operations = Synchronized(Nil: List[(String, String)])
+
+    def get: List[(String, String)] = print_operations.value
+
+    private def put(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    {
+      val ops =
+      {
+        import XML.Decode._
+        list(pair(string, string))(YXML.parse_body(msg.text))
+      }
+      print_operations.change(_ => ops)
+      true
+    }
+
+    override def start(prover: Prover): Unit =
+      prover.protocol_command(Markup.PRINT_OPERATIONS)
+
+    val functions = Map(Markup.PRINT_OPERATIONS -> put _)
+  }
+}
diff -r bc50d5e04e90 -r 1902d7c26017 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/build-jars	Mon May 05 17:48:55 2014 +0200
@@ -67,7 +67,6 @@
   PIDE/xml.scala
   PIDE/yxml.scala
   System/command_line.scala
-  System/interrupt.scala
   System/invoke_scala.scala
   System/isabelle_charset.scala
   System/isabelle_font.scala
@@ -75,6 +74,7 @@
   System/isabelle_system.scala
   System/options.scala
   System/platform.scala
+  System/posix_interrupt.scala
   System/system_channel.scala
   System/utf8.scala
   Thy/html.scala
@@ -89,6 +89,7 @@
   Tools/keywords.scala
   Tools/main.scala
   Tools/ml_statistics.scala
+  Tools/print_operation.scala
   Tools/simplifier_trace.scala
   Tools/task_statistics.scala
   library.scala
diff -r bc50d5e04e90 -r 1902d7c26017 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon May 05 10:03:43 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon May 05 17:48:55 2014 +0200
@@ -254,7 +254,7 @@
 
       val buffer = text_area.getBuffer
       val range = item.range
-      if (buffer.isEditable && range.length > 0) {
+      if (buffer.isEditable) {
         JEdit_Lib.buffer_edit(buffer) {
           JEdit_Lib.try_get_text(buffer, range) match {
             case Some(text) if text == item.original =>
@@ -524,7 +524,7 @@
       Swing_Thread.require {}
 
       val range = item.range
-      if (text_field.isEditable && range.length > 0) {
+      if (text_field.isEditable) {
         val content = text_field.getText
         JEdit_Lib.try_get_text(content, range) match {
           case Some(text) if text == item.original =>
diff -r bc50d5e04e90 -r 1902d7c26017 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Mon May 05 10:03:43 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Mon May 05 17:48:55 2014 +0200
@@ -184,9 +184,78 @@
   }
 
 
+  /* print operation */
+
+  private case class Print_Item(name: String, description: String)
+  {
+    override def toString: String = description
+  }
+
+  private val print_operation = new Find_Dockable.Operation(view)
+  {
+    /* query */
+
+    val query_operation =
+      new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
+        (snapshot, results, body) =>
+          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+    private var _selector_item: Option[Print_Item] = None
+    private var _selector = new ComboBox[Print_Item](Nil)
+
+    private def apply_query()
+    {
+      query_operation.apply_query(List(_selector.selection.item.name))
+    }
+
+    private val query_label = new Label("Print:")
+
+    def query: JComponent = _selector.peer.asInstanceOf[JComponent]
+
+
+    /* GUI page */
+
+    private def update_selector()
+    {
+      val items = Print_Operation.print_operations(PIDE.session).map(p => Print_Item(p._1, p._2))
+      _selector =
+        new ComboBox(items) {
+          _selector_item.foreach(item => selection.item = item)
+          listenTo(selection)
+          reactions += {
+            case SelectionChanged(_) =>
+              _selector_item = Some(selection.item)
+              apply_query()
+          }
+        }
+    }
+    update_selector()
+
+    private val apply_button = new Button("Apply") {
+      tooltip = "Apply to current context"
+      reactions += { case ButtonClicked(_) => apply_query() }
+    }
+
+    private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
+
+    def select
+    {
+      update_selector()
+      control_panel.contents.clear
+      control_panel.contents ++= List(query_label, _selector, apply_button, zoom)
+    }
+
+    val page =
+      new TabbedPane.Page("Print ...", new BorderPanel {
+        add(control_panel, BorderPanel.Position.North)
+        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+      }, "Print information from context")
+  }
+
+
   /* operations */
 
-  private val operations = List(find_theorems, find_consts)
+  private val operations = List(find_theorems, find_consts, print_operation)
 
   private val operations_pane = new TabbedPane
   {
@@ -200,7 +269,7 @@
     catch { case _: IndexOutOfBoundsException => None }
 
   private def select_operation() {
-    for (op <- get_operation()) op.select
+    for (op <- get_operation()) { op.select; op.query.requestFocus }
     operations_pane.revalidate
   }
 
diff -r bc50d5e04e90 -r 1902d7c26017 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon May 05 10:03:43 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon May 05 17:48:55 2014 +0200
@@ -124,7 +124,7 @@
           val (text, rendering) =
             try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
             catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
-          Simple_Thread.interrupted_exception()
+          Exn.Interrupt.expose()
 
           Swing_Thread.later {
             current_rendering = rendering