# HG changeset patch
# User wenzelm
# Date 1355345442 -3600
# Node ID 6647ba2775c1706eb4fb03c5da3f352a34310f2c
# Parent  492953de3090931573afcbd90ce49ecb360e2e81
support dialog via document content;

diff -r 492953de3090 -r 6647ba2775c1 src/Pure/PIDE/active.ML
--- a/src/Pure/PIDE/active.ML	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Pure/PIDE/active.ML	Wed Dec 12 21:50:42 2012 +0100
@@ -11,27 +11,54 @@
   val markup: string -> string -> string
   val sendback_markup_implicit: string -> string
   val sendback_markup: string -> string
+  val dialog: unit -> (string -> Markup.T) * string future
+  val dialog_result: string -> string -> unit
 end;
 
 structure Active: ACTIVE =
 struct
 
+(* active markup *)
+
+fun explicit_id () =
+  (case Position.get_id (Position.thread_data ()) of
+    SOME id => [(Markup.idN, id)]
+  | NONE => []);
+
 fun make_markup name {implicit, properties} =
   (name, [])
-  |> not implicit ? (fn markup =>
-      let
-        val props =
-          (case Position.get_id (Position.thread_data ()) of
-            SOME id => [(Markup.idN, id)]
-          | NONE => []);
-      in Markup.properties props markup end)
+  |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
   |> Markup.properties properties;
 
 fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
 fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
 
+
+(* sendback area *)
+
 val sendback_markup_implicit = markup_implicit Markup.sendbackN;
 val sendback_markup = markup Markup.sendbackN;
 
+
+(* dialog via document content *)
+
+val new_name = string_of_int o Synchronized.counter ();
+
+val dialogs = Synchronized.var "Active.dialogs" (Symtab.empty: string future Symtab.table);
+
+fun dialog () =
+  let
+    val name = new_name ();
+    fun abort () = Synchronized.change dialogs (Symtab.delete_safe name);
+    val promise = Future.promise abort : string future;
+    val _ = Synchronized.change dialogs (Symtab.update_new (name, promise));
+    fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog name result);
+  in (mk_markup, promise) end;
+
+fun dialog_result name result =
+  Synchronized.change_result dialogs
+    (fn tab => (Symtab.lookup tab name, Symtab.delete_safe name tab))
+  |> (fn NONE => () | SOME promise => Future.fulfill promise result);
+
 end;
 
diff -r 492953de3090 -r 6647ba2775c1 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Dec 12 21:50:42 2012 +0100
@@ -99,6 +99,7 @@
   val paddingN: string
   val padding_line: string * string
   val sendbackN: string
+  val dialogN: string val dialog: string -> string -> T
   val graphviewN: string
   val intensifyN: string val intensify: T
   val taskN: string
@@ -338,9 +339,13 @@
 val (subgoalN, subgoal) = markup_elem "subgoal";
 
 
-(* active areads *)
+(* active areas *)
 
 val sendbackN = "sendback";
+
+val dialogN = "dialog";
+fun dialog name result = (dialogN, [(nameN, name), ("result", result)]);
+
 val graphviewN = "graphview";
 
 val paddingN = "padding";
diff -r 492953de3090 -r 6647ba2775c1 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Dec 12 21:50:42 2012 +0100
@@ -216,6 +216,11 @@
   /* active areas */
 
   val SENDBACK = "sendback"
+
+  val DIALOG = "dialog"
+  val DIALOG_RESULT = "dialog_result"
+  val Result = new Properties.String("result")
+
   val GRAPHVIEW = "graphview"
 
   val PADDING = "padding"
diff -r 492953de3090 -r 6647ba2775c1 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Dec 12 21:50:42 2012 +0100
@@ -76,6 +76,12 @@
       in state1 end));
 
 val _ =
+  Isabelle_Process.protocol_command "Document.dialog_result"
+    (fn [name, result] =>
+      Active.dialog_result name result
+        handle exn => if Exn.is_interrupt exn then () else reraise exn);
+
+val _ =
   Isabelle_Process.protocol_command "Document.invoke_scala"
     (fn [id, tag, res] =>
       Invoke_Scala.fulfill_method id tag res
diff -r 492953de3090 -r 6647ba2775c1 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Dec 12 21:50:42 2012 +0100
@@ -269,6 +269,14 @@
   }
 
 
+  /* dialog via document content */
+
+  def dialog_result(name: String, result: String)
+  {
+    input("Document.dialog_result", name, result)
+  }
+
+
   /* method invocation service */
 
   def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
diff -r 492953de3090 -r 6647ba2775c1 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Pure/ROOT.ML	Wed Dec 12 21:50:42 2012 +0100
@@ -63,7 +63,6 @@
 
 use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
-use "PIDE/active.ML";
 
 use "General/graph.ML";
 
@@ -252,6 +251,7 @@
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
 use "Thy/thy_syntax.ML";
+use "PIDE/active.ML";
 use "PIDE/command.ML";
 use "Isar/outer_syntax.ML";
 use "General/graph_display.ML";
diff -r 492953de3090 -r 6647ba2775c1 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) }
 }
diff -r 492953de3090 -r 6647ba2775c1 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Tools/jEdit/etc/options	Wed Dec 12 21:50:42 2012 +0100
@@ -43,6 +43,7 @@
 option hyperlink_color : string = "000000FF"
 option active_color : string = "DCDCDCFF"
 option active_hover_color : string = "9DC75DFF"
+option active_result_color : string = "666633FF"
 option keyword1_color : string = "006699FF"
 option keyword2_color : string = "009966FF"
 
diff -r 492953de3090 -r 6647ba2775c1 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Tools/jEdit/src/active.scala	Wed Dec 12 21:50:42 2012 +0100
@@ -54,6 +54,13 @@
                     else text_area.setSelectedText(text)
                 }
 
+              case XML.Elem(Markup(Markup.DIALOG, props), _) =>
+                (props, props, props) match {
+                  case (Position.Id(id), Markup.Name(name), Markup.Result(result)) =>
+                    model.session.dialog_result(id, name, result)
+                  case _ =>
+                }
+
               case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) =>
                 default_thread_pool.submit(() =>
                   {
diff -r 492953de3090 -r 6647ba2775c1 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Dec 12 21:50:42 2012 +0100
@@ -137,6 +137,7 @@
   val hyperlink_color = color_value("hyperlink_color")
   val active_color = color_value("active_color")
   val active_hover_color = color_value("active_hover_color")
+  val active_result_color = color_value("active_result_color")
   val keyword1_color = color_value("keyword1_color")
   val keyword2_color = color_value("keyword2_color")
 
@@ -249,7 +250,8 @@
   }
 
 
-  private val active_include = Set(Markup.SENDBACK, Markup.GRAPHVIEW)
+  private val active_include =
+    Set(Markup.SENDBACK, Markup.DIALOG, Markup.DIALOG_RESULT, Markup.GRAPHVIEW)
 
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
     snapshot.select_markup(range, Some(active_include),
@@ -426,6 +428,8 @@
                 (None, Some(bad_color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                 (None, Some(intensify_color))
+              case (_, Text.Info(_, XML.Elem(Markup(Markup.DIALOG_RESULT, _), _))) =>
+                (None, Some(active_result_color))
               case (_, Text.Info(_, XML.Elem(Markup(name, _), _))) if active_include(name) =>
                 (None, Some(active_color))
             })