src/Pure/PIDE/active.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 50498 6647ba2775c1
child 50500 c94bba7906d2
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     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_implicit: string -> string
    13   val sendback_markup: string -> string
    14   val dialog: unit -> (string -> Markup.T) * string future
    15   val dialog_result: string -> 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 
    37 (* sendback area *)
    38 
    39 val sendback_markup_implicit = markup_implicit Markup.sendbackN;
    40 val sendback_markup = markup Markup.sendbackN;
    41 
    42 
    43 (* dialog via document content *)
    44 
    45 val new_name = string_of_int o Synchronized.counter ();
    46 
    47 val dialogs = Synchronized.var "Active.dialogs" (Symtab.empty: string future Symtab.table);
    48 
    49 fun dialog () =
    50   let
    51     val name = new_name ();
    52     fun abort () = Synchronized.change dialogs (Symtab.delete_safe name);
    53     val promise = Future.promise abort : string future;
    54     val _ = Synchronized.change dialogs (Symtab.update_new (name, promise));
    55     fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog name result);
    56   in (mk_markup, promise) end;
    57 
    58 fun dialog_result name result =
    59   Synchronized.change_result dialogs
    60     (fn tab => (Symtab.lookup tab name, Symtab.delete_safe name tab))
    61   |> (fn NONE => () | SOME promise => Future.fulfill promise result);
    62 
    63 end;
    64