--- 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;
--- 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";
--- 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"
--- 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
--- 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)
--- 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";
--- 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) }
}
--- 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"
--- 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(() =>
{
--- 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))
})