src/Pure/PIDE/active.ML
author wenzelm
Thu Dec 13 18:00:24 2012 +0100 (2012-12-13 ago)
changeset 50503 50f141b34bb7
parent 50500 c94bba7906d2
child 50504 2cc6eab90cdf
permissions -rw-r--r--
enable Isabelle/ML to produce uninterpreted result messages as well;
     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: 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 
    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 dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
    46 
    47 fun dialog () =
    48   let
    49     val i = serial ();
    50     fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
    51     val promise = Future.promise abort : string future;
    52     val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
    53     fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
    54   in (mk_markup, promise) end;
    55 
    56 fun dialog_result i result =
    57   Synchronized.change_result dialogs
    58     (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
    59   |> (fn NONE => () | SOME promise => Future.fulfill promise result);
    60 
    61 end;
    62