src/Pure/PIDE/active.ML
author wenzelm
Tue Aug 28 11:40:11 2018 +0200 (11 months ago ago)
changeset 68829 1a4fa494a4a8
parent 66167 c88d1c36c9c3
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/PIDE/active.ML
     2     Author:     Makarius
     3 
     4 Active areas within the document (see also Tools/jEdit/src/active.scala).
     5 *)
     6 
     7 signature ACTIVE =
     8 sig
     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
    17 end;
    18 
    19 structure Active: ACTIVE =
    20 struct
    21 
    22 (* active markup *)
    23 
    24 fun explicit_id () = Position.id_properties_of (Position.thread_data ());
    25 
    26 fun make_markup name {implicit, properties} =
    27   (name, [])
    28   |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
    29   |> Markup.properties properties;
    30 
    31 fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
    32 fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
    33 
    34 fun sendback_markup_properties props s =
    35   Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props}) s;
    36 
    37 fun sendback_markup_command s =
    38   sendback_markup_properties [Markup.padding_command] s;
    39 
    40 
    41 (* dialog via document content *)
    42 
    43 val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
    44 
    45 fun 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 
    54 fun dialog_text () =
    55   let val (markup, promise) = dialog ()
    56   in (fn s => Markup.markup (markup s) s, promise) end;
    57 
    58 fun 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 
    63 end;
    64