# HG changeset patch
# User wenzelm
# Date 1396943113 -7200
# Node ID 38d0b209974307bce0690a19cfaa3808aff6f462
# Parent  a8d960baa5c28ed1ae873324716a3912e198736d
no report for position singularity, notably for aux. file, especially empty one;

diff -r a8d960baa5c2 -r 38d0b2099743 src/Pure/General/position.ML
--- 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];
diff -r a8d960baa5c2 -r 38d0b2099743 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Apr 07 23:02:29 2014 +0200
+++ b/src/Pure/ML/ml_lex.ML	Tue Apr 08 09:45:13 2014 +0200
@@ -325,8 +325,12 @@
 val read = gen_read false;
 
 fun read_source SML {delimited, text, pos} =
-  (Position.report pos ((if SML then Markup.language_SML else Markup.language_ML) delimited);
-   gen_read SML pos text);
+  let
+    val language = if SML then Markup.language_SML else Markup.language_ML;
+    val _ =
+      if Position.is_reported_range pos then Position.report pos (language delimited)
+      else ();
+  in gen_read SML pos text end;
 
 end;