# HG changeset patch
# User wenzelm
# Date 1284055753 -7200
# Node ID a0c0698e56c06bf4f8320ac640938be2c8dd6b2d
# Parent  47273e5b1441e02f1efa217546f185faf255fbd8
ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;

diff -r 47273e5b1441 -r a0c0698e56c0 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Sep 09 18:32:21 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Sep 09 20:09:13 2010 +0200
@@ -25,6 +25,10 @@
     loc_props
   end |> Position.of_properties;
 
+fun offset_position_of loc =
+  let val pos = position_of loc
+  in if is_some (Position.offset_of pos) then pos else Position.none end;
+
 fun exn_position exn =
   (case PolyML.exceptionLocation exn of
     NONE => Position.none
@@ -44,12 +48,12 @@
       | _ => Position.report_text);
 
     fun report_decl markup loc decl =
-      report_text Markup.ML_ref (position_of loc)
+      report_text Markup.ML_ref (offset_position_of loc)
         (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
     fun report loc (PolyML.PTtype types) =
           PolyML.NameSpace.displayTypeExpression (types, depth, space)
           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
-          |> report_text Markup.ML_typing (position_of loc)
+          |> report_text Markup.ML_typing (offset_position_of loc)
       | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
       | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
       | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
@@ -116,12 +120,11 @@
 
     fun message {message = msg, hard, location = loc, context = _} =
       let
-        val pos = position_of loc;
         val txt =
           Markup.markup Markup.location
-            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
+            ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
           Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
-          Markup.markup (Position.report_markup pos) "";
+          Markup.markup (Position.report_markup (offset_position_of loc)) "";
       in if hard then err txt else warn txt end;