--- a/src/Pure/PIDE/active.ML Thu Dec 13 18:00:24 2012 +0100
+++ b/src/Pure/PIDE/active.ML Thu Dec 13 18:15:53 2012 +0100
@@ -50,8 +50,8 @@
fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
val promise = Future.promise abort : string future;
val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
- fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
- in (mk_markup, promise) end;
+ fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
+ in (result_markup, promise) end;
fun dialog_result i result =
Synchronized.change_result dialogs