# HG changeset patch
# User wenzelm
# Date 1355418953 -3600
# Node ID 2cc6eab90cdf3e387eb90b6e89ba19d131ce687f
# Parent  50f141b34bb798b40acad02db10b1716a9994365
tuned;

diff -r 50f141b34bb7 -r 2cc6eab90cdf src/Pure/PIDE/active.ML
--- 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