diff -r 67fb9a168d10 -r 97959912840a src/Pure/PIDE/sendback.ML
--- a/src/Pure/PIDE/sendback.ML	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Pure/PIDE/sendback.ML	Mon Nov 26 16:16:47 2012 +0100
@@ -7,7 +7,7 @@
 
 signature SENDBACK =
 sig
-  val make_markup: {implicit: bool} -> Markup.T
+  val make_markup: {implicit: bool, properties: Properties.T} -> Markup.T
   val markup_implicit: string -> string
   val markup: string -> string
 end;
@@ -15,18 +15,19 @@
 structure Sendback: SENDBACK =
 struct
 
-fun make_markup {implicit} =
-  if implicit then Markup.sendback
-  else
-    let
-      val props =
-        (case Position.get_id (Position.thread_data ()) of
-          SOME id => [(Markup.idN, id)]
-        | NONE => []);
-    in Markup.properties props Markup.sendback end;
+fun make_markup {implicit, properties} =
+  Markup.sendback
+  |> not implicit ? (fn markup =>
+      let
+        val props =
+          (case Position.get_id (Position.thread_data ()) of
+            SOME id => [(Markup.idN, id)]
+          | NONE => []);
+      in Markup.properties props markup end)
+  |> Markup.properties properties;
 
-fun markup_implicit s = Markup.markup (make_markup {implicit = true}) s;
-fun markup s = Markup.markup (make_markup {implicit = false}) s;
+fun markup_implicit s = Markup.markup (make_markup {implicit = true, properties = []}) s;
+fun markup s = Markup.markup (make_markup {implicit = false, properties = []}) s;
 
 end;