src/Pure/PIDE/active.ML
author wenzelm
Wed Dec 03 14:04:38 2014 +0100 (2014-12-03 ago)
changeset 59083 88b0b1f28adc
parent 52697 6fb98a20c349
child 63518 ae8fd6fe63a1
permissions -rw-r--r--
tuned signature;
wenzelm@50450
     1
(*  Title:      Pure/PIDE/active.ML
wenzelm@50163
     2
    Author:     Makarius
wenzelm@50163
     3
wenzelm@50450
     4
Active areas within the document (see also Tools/jEdit/src/active.scala).
wenzelm@50163
     5
*)
wenzelm@50163
     6
wenzelm@50450
     7
signature ACTIVE =
wenzelm@50163
     8
sig
wenzelm@50450
     9
  val make_markup: string -> {implicit: bool, properties: Properties.T} -> Markup.T
wenzelm@50450
    10
  val markup_implicit: string -> string -> string
wenzelm@50450
    11
  val markup: string -> string -> string
wenzelm@52697
    12
  val sendback_markup: Properties.T -> string -> string
wenzelm@50498
    13
  val dialog: unit -> (string -> Markup.T) * string future
wenzelm@50505
    14
  val dialog_text: unit -> (string -> string) * string future
wenzelm@50500
    15
  val dialog_result: serial -> string -> unit
wenzelm@50163
    16
end;
wenzelm@50163
    17
wenzelm@50450
    18
structure Active: ACTIVE =
wenzelm@50163
    19
struct
wenzelm@50163
    20
wenzelm@50498
    21
(* active markup *)
wenzelm@50498
    22
wenzelm@50498
    23
fun explicit_id () =
wenzelm@50498
    24
  (case Position.get_id (Position.thread_data ()) of
wenzelm@50498
    25
    SOME id => [(Markup.idN, id)]
wenzelm@50498
    26
  | NONE => []);
wenzelm@50498
    27
wenzelm@50450
    28
fun make_markup name {implicit, properties} =
wenzelm@50450
    29
  (name, [])
wenzelm@50498
    30
  |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
wenzelm@50215
    31
  |> Markup.properties properties;
wenzelm@50163
    32
wenzelm@50450
    33
fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
wenzelm@50450
    34
fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
wenzelm@50450
    35
wenzelm@52697
    36
fun sendback_markup props =
wenzelm@52697
    37
  Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props});
wenzelm@50164
    38
wenzelm@50498
    39
wenzelm@50498
    40
(* dialog via document content *)
wenzelm@50498
    41
wenzelm@50500
    42
val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
wenzelm@50498
    43
wenzelm@50498
    44
fun dialog () =
wenzelm@50498
    45
  let
wenzelm@50500
    46
    val i = serial ();
wenzelm@50500
    47
    fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
wenzelm@50498
    48
    val promise = Future.promise abort : string future;
wenzelm@50500
    49
    val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
wenzelm@50504
    50
    fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
wenzelm@50504
    51
  in (result_markup, promise) end;
wenzelm@50498
    52
wenzelm@50505
    53
fun dialog_text () =
wenzelm@50505
    54
  let val (markup, promise) = dialog ()
wenzelm@50505
    55
  in (fn s => Markup.markup (markup s) s, promise) end;
wenzelm@50505
    56
wenzelm@50500
    57
fun dialog_result i result =
wenzelm@50498
    58
  Synchronized.change_result dialogs
wenzelm@50500
    59
    (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
wenzelm@50498
    60
  |> (fn NONE => () | SOME promise => Future.fulfill promise result);
wenzelm@50498
    61
wenzelm@50163
    62
end;
wenzelm@50163
    63