--- 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;