src/Pure/PIDE/active.ML
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 68829 1a4fa494a4a8
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
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@68829
    24
fun explicit_id () = Position.id_properties_of (Position.thread_data ());
wenzelm@50498
    25
wenzelm@50450
    26
fun make_markup name {implicit, properties} =
wenzelm@50450
    27
  (name, [])
wenzelm@50498
    28
  |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
wenzelm@50215
    29
  |> Markup.properties properties;
wenzelm@50163
    30
wenzelm@50450
    31
fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
wenzelm@50450
    32
fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
wenzelm@50450
    33
wenzelm@63518
    34
fun sendback_markup_properties props s =
wenzelm@63518
    35
  Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props}) s;
wenzelm@63518
    36
wenzelm@63518
    37
fun sendback_markup_command s =
wenzelm@63518
    38
  sendback_markup_properties [Markup.padding_command] s;
wenzelm@50164
    39
wenzelm@50498
    40
wenzelm@50498
    41
(* dialog via document content *)
wenzelm@50498
    42
wenzelm@50500
    43
val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
wenzelm@50498
    44
wenzelm@50498
    45
fun dialog () =
wenzelm@50498
    46
  let
wenzelm@50500
    47
    val i = serial ();
wenzelm@50500
    48
    fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
wenzelm@66167
    49
    val promise = Future.promise_name "dialog" abort : string future;
wenzelm@50500
    50
    val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
wenzelm@50504
    51
    fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
wenzelm@50504
    52
  in (result_markup, promise) end;
wenzelm@50498
    53
wenzelm@50505
    54
fun dialog_text () =
wenzelm@50505
    55
  let val (markup, promise) = dialog ()
wenzelm@50505
    56
  in (fn s => Markup.markup (markup s) s, promise) end;
wenzelm@50505
    57
wenzelm@50500
    58
fun dialog_result i result =
wenzelm@50498
    59
  Synchronized.change_result dialogs
wenzelm@50500
    60
    (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
wenzelm@50498
    61
  |> (fn NONE => () | SOME promise => Future.fulfill promise result);
wenzelm@50498
    62
wenzelm@50163
    63
end;
wenzelm@50163
    64