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;
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@50450
    12
  val sendback_markup_implicit: string -> string
wenzelm@50450
    13
  val sendback_markup: string -> string
wenzelm@50498
    14
  val dialog: unit -> (string -> Markup.T) * string future
wenzelm@50500
    15
  val dialog_result: serial -> string -> unit
wenzelm@50163
    16
end;
wenzelm@50163
    17
wenzelm@50450
    18
structure Active: ACTIVE =
wenzelm@50163
    19
struct
wenzelm@50163
    20
wenzelm@50498
    21
(* active markup *)
wenzelm@50498
    22
wenzelm@50498
    23
fun explicit_id () =
wenzelm@50498
    24
  (case Position.get_id (Position.thread_data ()) of
wenzelm@50498
    25
    SOME id => [(Markup.idN, id)]
wenzelm@50498
    26
  | NONE => []);
wenzelm@50498
    27
wenzelm@50450
    28
fun make_markup name {implicit, properties} =
wenzelm@50450
    29
  (name, [])
wenzelm@50498
    30
  |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
wenzelm@50215
    31
  |> Markup.properties properties;
wenzelm@50163
    32
wenzelm@50450
    33
fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
wenzelm@50450
    34
fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
wenzelm@50450
    35
wenzelm@50498
    36
wenzelm@50498
    37
(* sendback area *)
wenzelm@50498
    38
wenzelm@50450
    39
val sendback_markup_implicit = markup_implicit Markup.sendbackN;
wenzelm@50450
    40
val sendback_markup = markup Markup.sendbackN;
wenzelm@50164
    41
wenzelm@50498
    42
wenzelm@50498
    43
(* dialog via document content *)
wenzelm@50498
    44
wenzelm@50500
    45
val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
wenzelm@50498
    46
wenzelm@50498
    47
fun dialog () =
wenzelm@50498
    48
  let
wenzelm@50500
    49
    val i = serial ();
wenzelm@50500
    50
    fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
wenzelm@50498
    51
    val promise = Future.promise abort : string future;
wenzelm@50500
    52
    val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
wenzelm@50500
    53
    fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
wenzelm@50498
    54
  in (mk_markup, promise) end;
wenzelm@50498
    55
wenzelm@50500
    56
fun dialog_result i result =
wenzelm@50498
    57
  Synchronized.change_result dialogs
wenzelm@50500
    58
    (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
wenzelm@50498
    59
  |> (fn NONE => () | SOME promise => Future.fulfill promise result);
wenzelm@50498
    60
wenzelm@50163
    61
end;
wenzelm@50163
    62