--- a/src/Pure/General/position.ML Mon Apr 07 23:02:29 2014 +0200
+++ b/src/Pure/General/position.ML Tue Apr 08 09:45:13 2014 +0200
@@ -35,6 +35,7 @@
val default_properties: T -> Properties.T -> Properties.T
val markup: T -> Markup.T -> Markup.T
val is_reported: T -> bool
+ val is_reported_range: T -> bool
val reported_text: T -> Markup.T -> string -> string
val report_text: T -> Markup.T -> string -> unit
val report: T -> Markup.T -> unit
@@ -166,6 +167,7 @@
(* reports *)
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
+fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
fun report_text pos markup txt = Output.report [reported_text pos markup txt];