1(*  Title:      Pure/PIDE/active.ML
2    Author:     Makarius
3
4Active areas within the document (see also Tools/jEdit/src/active.scala).
5*)
6
7signature ACTIVE =
8sig
9  val make_markup: string -> {implicit: bool, properties: Properties.T} -> Markup.T
10  val markup_implicit: string -> string -> string
11  val markup: string -> string -> string
12  val sendback_markup_properties: Properties.T -> string -> string
13  val sendback_markup_command: string -> string
14  val dialog: unit -> (string -> Markup.T) * string future
15  val dialog_text: unit -> (string -> string) * string future
16  val dialog_result: serial -> string -> unit
17end;
18
19structure Active: ACTIVE =
20struct
21
22(* active markup *)
23
24fun explicit_id () = Position.id_properties_of (Position.thread_data ());
25
26fun make_markup name {implicit, properties} =
27  (name, [])
28  |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
29  |> Markup.properties properties;
30
31fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
32fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
33
34fun sendback_markup_properties props s =
35  Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props}) s;
36
37fun sendback_markup_command s =
38  sendback_markup_properties [Markup.padding_command] s;
39
40
41(* dialog via document content *)
42
43val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
44
45fun dialog () =
46  let
47    val i = serial ();
48    fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
49    val promise = Future.promise_name "dialog" abort : string future;
50    val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
51    fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
52  in (result_markup, promise) end;
53
54fun dialog_text () =
55  let val (markup, promise) = dialog ()
56  in (fn s => Markup.markup (markup s) s, promise) end;
57
58fun dialog_result i result =
59  Synchronized.change_result dialogs
60    (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
61  |> (fn NONE => () | SOME promise => Future.fulfill promise result);
62
63end;
64
65