# HG changeset patch
# User wenzelm
# Date 1294759408 -3600
# Node ID f0f20a5b54df254b25706e590c83933d3bd3bb14
# Parent  a7462e442e35363e86849d76b8fb53e5fd33b157
clarified notion Position.is_reported;
ML warning/error: retain non-reported clear-text position, notably when evaluating external ML files;

diff -r a7462e442e35 -r f0f20a5b54df src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Jan 10 22:03:24 2011 +0100
+++ b/src/Pure/General/position.ML	Tue Jan 11 16:23:28 2011 +0100
@@ -30,6 +30,7 @@
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
+  val is_reported: T -> bool
   val reported_text: T -> Markup.T -> string -> string
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
@@ -148,10 +149,9 @@
 
 (* reports *)
 
-fun reported_text (pos as Pos (count, _)) m txt =
-  if invalid_count count then ""
-  else Markup.markup (markup pos m) txt;
+fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id 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);
 fun report pos markup = report_text pos markup "";
 
diff -r a7462e442e35 -r f0f20a5b54df src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Jan 10 22:03:24 2011 +0100
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Jan 11 16:23:28 2011 +0100
@@ -22,10 +22,6 @@
       {line = line, column = 0, offset = offset, end_offset = end_offset, props = props}
   end;
 
-fun offset_position_of (loc: PolyML.location) =
-  if #startPosition loc > 0 then position_of loc
-  else Position.none;
-
 fun exn_position exn =
   (case PolyML.exceptionLocation exn of
     NONE => Position.none
@@ -45,14 +41,14 @@
       | _ => Position.report_text);
 
     fun report_decl markup loc decl =
-      report_text (offset_position_of loc) Markup.ML_ref
+      report_text (position_of loc) Markup.ML_ref
         (Markup.markup (Position.markup (position_of decl) markup) "");
 
     fun report loc (PolyML.PTtype types) =
           cons (fn () =>
             PolyML.NameSpace.displayTypeExpression (types, depth, space)
             |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
-            |> report_text (offset_position_of loc) Markup.ML_typing)
+            |> report_text (position_of loc) Markup.ML_typing)
       | report loc (PolyML.PTdeclaredAt decl) = cons (fn () => report_decl Markup.ML_def loc decl)
       | report loc (PolyML.PTopenedAt decl) = cons (fn () => report_decl Markup.ML_open loc decl)
       | report loc (PolyML.PTstructureAt decl) =
@@ -112,11 +108,12 @@
 
     fun message {message = msg, hard, location = loc, context = _} =
       let
+        val pos = position_of loc;
         val txt =
-          Markup.markup Markup.no_report
-            ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
+          (Position.is_reported pos ? Markup.markup Markup.no_report)
+            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
           Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
-          Position.reported_text (offset_position_of loc)  Markup.report "";
+          Position.reported_text pos Markup.report "";
       in if hard then err txt else warn txt end;