--- a/src/Pure/PIDE/sendback.ML Mon Nov 26 11:42:16 2012 +0100
+++ b/src/Pure/PIDE/sendback.ML Mon Nov 26 11:59:56 2012 +0100
@@ -7,25 +7,26 @@
signature SENDBACK =
sig
- val make_markup: unit -> Markup.T
+ val make_markup: {implicit: bool} -> Markup.T
+ val markup_implicit: string -> string
val markup: string -> string
- val markup_implicit: string -> string
end;
structure Sendback: SENDBACK =
struct
-fun make_markup () =
- 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} =
+ 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 markup s = Markup.markup (make_markup ()) s;
-
-fun markup_implicit s = Markup.markup Markup.sendback s;
+fun markup_implicit s = Markup.markup (make_markup {implicit = true}) s;
+fun markup s = Markup.markup (make_markup {implicit = false}) s;
end;