src/Pure/PIDE/active.ML

--- a/src/Pure/PIDE/active.ML	Thu Dec 13 18:15:53 2012 +0100
+++ b/src/Pure/PIDE/active.ML	Thu Dec 13 19:53:55 2012 +0100
@@ -12,6 +12,7 @@
   val sendback_markup_implicit: string -> string
   val sendback_markup: string -> string
   val dialog: unit -> (string -> Markup.T) * string future
+  val dialog_text: unit -> (string -> string) * string future
   val dialog_result: serial -> string -> unit
 end;
 
@@ -53,6 +54,10 @@
     fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
   in (result_markup, promise) end;
 
+fun dialog_text () =
+  let val (markup, promise) = dialog ()
+  in (fn s => Markup.markup (markup s) s, promise) end;
+
 fun dialog_result i result =
   Synchronized.change_result dialogs
     (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))