src/Pure/PIDE/active.ML

--- a/src/Pure/PIDE/active.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/Pure/PIDE/active.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -9,8 +9,7 @@
   val make_markup: string -> {implicit: bool, properties: Properties.T} -> Markup.T
   val markup_implicit: string -> string -> string
   val markup: string -> string -> string
-  val sendback_markup_implicit: string -> string
-  val sendback_markup: string -> string
+  val sendback_markup: Properties.T -> string -> string
   val dialog: unit -> (string -> Markup.T) * string future
   val dialog_text: unit -> (string -> string) * string future
   val dialog_result: serial -> string -> unit
@@ -34,11 +33,8 @@
 fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
 fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
 
-
-(* sendback area *)
-
-val sendback_markup_implicit = markup_implicit Markup.sendbackN;
-val sendback_markup = markup Markup.sendbackN;
+fun sendback_markup props =
+  Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props});
 
 
 (* dialog via document content *)