src/Pure/System/session.scala

--- a/src/Pure/System/session.scala	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Pure/System/session.scala	Wed Dec 12 21:50:42 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, name: String, result: String)
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
@@ -419,6 +420,14 @@
 
           reply(())
 
+        case Session.Dialog_Result(id, name, result) if prover.isDefined =>
+          prover.get.dialog_result(name, result)
+
+          val dialog_result =
+            XML.Elem(Markup(Markup.DIALOG_RESULT, Markup.Name(name) ::: Markup.Result(result)), Nil)
+          handle_output(new Isabelle_Process.Output(
+            XML.Elem(Markup(Markup.REPORT, Position.Id(id)), List(dialog_result))))
+
         case Messages(msgs) =>
           msgs foreach {
             case input: Isabelle_Process.Input =>
@@ -469,4 +478,7 @@
 
   def update(edits: List[Document.Edit_Text])
   { session_actor !? Session.Raw_Edits(edits) }
+
+  def dialog_result(id: Document.ID, name: String, result: String)
+  { session_actor ! Session.Dialog_Result(id, name, result) }
 }