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