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