src/Pure/PIDE/active.ML
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 63518 ae8fd6fe63a1
child 66167 c88d1c36c9c3
permissions -rw-r--r--
clarified modules;
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@63518
    12
  val sendback_markup_properties: Properties.T -> string -> string
wenzelm@63518
    13
  val sendback_markup_command: string -> string
wenzelm@50498
    14
  val dialog: unit -> (string -> Markup.T) * string future
wenzelm@50505
    15
  val dialog_text: unit -> (string -> string) * string future
wenzelm@50500
    16
  val dialog_result: serial -> string -> unit
wenzelm@50163
    17
end;
wenzelm@50163
    18
wenzelm@50450
    19
structure Active: ACTIVE =
wenzelm@50163
    20
struct
wenzelm@50163
    21
wenzelm@50498
    22
(* active markup *)
wenzelm@50498
    23
wenzelm@50498
    24
fun explicit_id () =
wenzelm@50498
    25
  (case Position.get_id (Position.thread_data ()) of
wenzelm@50498
    26
    SOME id => [(Markup.idN, id)]
wenzelm@50498
    27
  | NONE => []);
wenzelm@50498
    28
wenzelm@50450
    29
fun make_markup name {implicit, properties} =
wenzelm@50450
    30
  (name, [])
wenzelm@50498
    31
  |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
wenzelm@50215
    32
  |> Markup.properties properties;
wenzelm@50163
    33
wenzelm@50450
    34
fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
wenzelm@50450
    35
fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
wenzelm@50450
    36
wenzelm@63518
    37
fun sendback_markup_properties props s =
wenzelm@63518
    38
  Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props}) s;
wenzelm@63518
    39
wenzelm@63518
    40
fun sendback_markup_command s =
wenzelm@63518
    41
  sendback_markup_properties [Markup.padding_command] s;
wenzelm@50164
    42
wenzelm@50498
    43
wenzelm@50498
    44
(* dialog via document content *)
wenzelm@50498
    45
wenzelm@50500
    46
val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
wenzelm@50498
    47
wenzelm@50498
    48
fun dialog () =
wenzelm@50498
    49
  let
wenzelm@50500
    50
    val i = serial ();
wenzelm@50500
    51
    fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
wenzelm@50498
    52
    val promise = Future.promise abort : string future;
wenzelm@50500
    53
    val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
wenzelm@50504
    54
    fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
wenzelm@50504
    55
  in (result_markup, promise) end;
wenzelm@50498
    56
wenzelm@50505
    57
fun dialog_text () =
wenzelm@50505
    58
  let val (markup, promise) = dialog ()
wenzelm@50505
    59
  in (fn s => Markup.markup (markup s) s, promise) end;
wenzelm@50505
    60
wenzelm@50500
    61
fun dialog_result i result =
wenzelm@50498
    62
  Synchronized.change_result dialogs
wenzelm@50500
    63
    (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
wenzelm@50498
    64
  |> (fn NONE => () | SOME promise => Future.fulfill promise result);
wenzelm@50498
    65
wenzelm@50163
    66
end;
wenzelm@50163
    67