cancel_query via direct access to the exec_id of the running query process;

--- a/src/Pure/PIDE/protocol.ML	Fri Aug 09 10:41:17 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Aug 09 11:18:36 2013 +0200
@@ -32,6 +32,10 @@
     (fn [] => Execution.discontinue ());
 
 val _ =
+  Isabelle_Process.protocol_command "Document.cancel_exec"
+    (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id));
+
+val _ =
   Isabelle_Process.protocol_command "Document.update"
     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let

--- a/src/Pure/PIDE/protocol.scala	Fri Aug 09 10:41:17 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Aug 09 11:18:36 2013 +0200
@@ -315,9 +315,16 @@
       Document_ID(command.id), encode(command.name), encode(command.source))
 
 
-  /* document versions */
+  /* execution */
+
+  def discontinue_execution(): Unit =
+    protocol_command("Document.discontinue_execution")
 
-  def discontinue_execution() { protocol_command("Document.discontinue_execution") }
+  def cancel_exec(id: Document_ID.Exec): Unit =
+    protocol_command("Document.cancel_exec", Document_ID(id))
+
+
+  /* document versions */
 
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     edits: List[Document.Edit_Command])
@@ -363,8 +370,6 @@
 
   /* dialog via document content */
 
-  def dialog_result(serial: Long, result: String)
-  {
+  def dialog_result(serial: Long, result: String): Unit =
     protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
-  }
 }

--- a/src/Pure/PIDE/query_operation.ML	Fri Aug 09 10:41:17 2013 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Fri Aug 09 11:18:36 2013 +0200
@@ -18,7 +18,7 @@
   Command.print_function name
     (fn {args = instance :: args, ...} =>
         SOME {delay = NONE, pri = 0, persistent = false,
-          print_fn = fn _ => fn state =>
+          print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
             let
               fun result s = Output.result [(Markup.instanceN, instance)] s;
               fun status m = result (Markup.markup_only m);
@@ -26,13 +26,15 @@
                 result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn));
 
               val _ = status Markup.running;
-              val outputs = f state args handle exn (*sic!*) => (toplevel_error exn; []);
+              val outputs =
+                Multithreading.interruptible (fn () => f state args) ()
+                  handle exn (*sic!*) => (toplevel_error exn; []);
               val _ = outputs |> Par_List.map (fn out =>
-                (case Exn.capture out () (*sic!*) of
+                (case Exn.capture (restore_attributes out) () (*sic!*) of
                   Exn.Res s => result (Markup.markup (Markup.writelnN, []) s)
                 | Exn.Exn exn => toplevel_error exn));
               val _ = status Markup.finished;
-            in () end}
+            in () end)}
       | _ => NONE);
 
 fun register name f =

--- a/src/Pure/System/session.scala	Fri Aug 09 10:41:17 2013 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 09 11:18:36 2013 +0200
@@ -238,6 +238,7 @@
   /* actor messages */
 
   private case class Start(args: List[String])
+  private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Change(
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
@@ -506,6 +507,9 @@
           global_options.event(Session.Global_Options(options))
           reply(())
 
+        case Cancel_Exec(exec_id) if prover.isDefined =>
+          prover.get.cancel_exec(exec_id)
+
         case Session.Raw_Edits(edits) if prover.isDefined =>
           handle_raw_edits(edits)
           reply(())
@@ -552,6 +556,8 @@
     session_actor !? Stop
   }
 
+  def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
+
   def update(edits: List[Document.Edit_Text])
   { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
 

--- a/src/Tools/jEdit/src/query_operation.scala	Fri Aug 09 10:41:17 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Fri Aug 09 11:18:36 2013 +0200
@@ -48,6 +48,7 @@
   private var current_update_pending = false
   private var current_output: List[XML.Tree] = Nil
   private var current_status = Status.FINISHED
+  private var current_exec_id = Document_ID.none
 
   private def reset_state()
   {
@@ -56,6 +57,7 @@
     current_update_pending = false
     current_output = Nil
     current_status = Status.FINISHED
+    current_exec_id = Document_ID.none
   }
 
   private def remove_overlay()
@@ -123,31 +125,37 @@
 
     val results =
       (for {
-        (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- state.results.entries
+        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
         if props.contains((Markup.INSTANCE, instance))
-      } yield body).toList
+      } yield elem).toList
 
 
     /* output */
 
     val new_output =
       for {
-        List(XML.Elem(markup, body)) <- results
+        XML.Elem(_, List(XML.Elem(markup, body))) <- results
         if Markup.messages.contains(markup.name)
-      }
-      yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
+      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
 
 
     /* status */
 
     def get_status(name: String, status: Status.Value): Option[Status.Value] =
-      results.collectFirst({ case List(elem: XML.Elem) if elem.name == name => status })
+      results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
 
     val new_status =
       get_status(Markup.FINISHED, Status.FINISHED) orElse
       get_status(Markup.RUNNING, Status.RUNNING) getOrElse
       Status.WAITING
 
+    if (new_status == Status.RUNNING)
+      results.collectFirst(
+      {
+        case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
+        if elem.name == Markup.RUNNING => id
+      }).foreach(id => current_exec_id = id)
+
 
     /* state update */
 
@@ -173,7 +181,10 @@
   }
 
 
-  /* apply query */
+  /* query operations */
+
+  def cancel_query(): Unit =
+    Swing_Thread.require { PIDE.session.cancel_exec(current_exec_id) }
 
   def apply_query(query: List[String])
   {
@@ -198,9 +209,6 @@
     }
   }
 
-
-  /* locate query */
-
   def locate_query()
   {
     Swing_Thread.require()

--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 09 10:41:17 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 09 11:18:36 2013 +0200
@@ -127,6 +127,11 @@
     reactions += { case ButtonClicked(_) => clicked }
   }
 
+  private val cancel_query = new Button("Cancel") {
+    tooltip = "Interrupt unfinished query process"
+    reactions += { case ButtonClicked(_) => sledgehammer.cancel_query() }
+  }
+
   private val locate_query = new Button("Locate") {
     tooltip = "Locate context of current query within source text"
     reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
@@ -139,6 +144,6 @@
   private val controls =
     new FlowPanel(FlowPanel.Alignment.Right)(
       provers_label, Component.wrap(provers), timeout, subgoal, isar_proofs,
-      sledgehammer.animation, apply_query, locate_query, zoom)
+      sledgehammer.animation, apply_query, cancel_query, locate_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }