1.1 --- a/src/Pure/General/position.ML	Tue Jan 11 14:14:13 2011 +0100
     1.2 +++ b/src/Pure/General/position.ML	Tue Jan 11 17:00:21 2011 +0100
     1.3 @@ -30,6 +30,7 @@
     1.4    val properties_of: T -> Properties.T
     1.5    val default_properties: T -> Properties.T -> Properties.T
     1.6    val markup: T -> Markup.T -> Markup.T
     1.7 +  val is_reported: T -> bool
     1.8    val reported_text: T -> Markup.T -> string -> string
     1.9    val report_text: T -> Markup.T -> string -> unit
    1.10    val report: T -> Markup.T -> unit
    1.11 @@ -148,10 +149,9 @@
    1.12  
    1.13  (* reports *)
    1.14  
    1.15 -fun reported_text (pos as Pos (count, _)) m txt =
    1.16 -  if invalid_count count then ""
    1.17 -  else Markup.markup (markup pos m) txt;
    1.18 +fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
    1.19  
    1.20 +fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
    1.21  fun report_text pos markup txt = Output.report (reported_text pos markup txt);
    1.22  fun report pos markup = report_text pos markup "";
    1.23  

     2.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Jan 11 14:14:13 2011 +0100
     2.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Jan 11 17:00:21 2011 +0100
     2.3 @@ -22,10 +22,6 @@
     2.4        {line = line, column = 0, offset = offset, end_offset = end_offset, props = props}
     2.5    end;
     2.6  
     2.7 -fun offset_position_of (loc: PolyML.location) =
     2.8 -  if #startPosition loc > 0 then position_of loc
     2.9 -  else Position.none;
    2.10 -
    2.11  fun exn_position exn =
    2.12    (case PolyML.exceptionLocation exn of
    2.13      NONE => Position.none
    2.14 @@ -45,14 +41,14 @@
    2.15        | _ => Position.report_text);
    2.16  
    2.17      fun report_decl markup loc decl =
    2.18 -      report_text (offset_position_of loc) Markup.ML_ref
    2.19 +      report_text (position_of loc) Markup.ML_ref
    2.20          (Markup.markup (Position.markup (position_of decl) markup) "");
    2.21  
    2.22      fun report loc (PolyML.PTtype types) =
    2.23            cons (fn () =>
    2.24              PolyML.NameSpace.displayTypeExpression (types, depth, space)
    2.25              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    2.26 -            |> report_text (offset_position_of loc) Markup.ML_typing)
    2.27 +            |> report_text (position_of loc) Markup.ML_typing)
    2.28        | report loc (PolyML.PTdeclaredAt decl) = cons (fn () => report_decl Markup.ML_def loc decl)
    2.29        | report loc (PolyML.PTopenedAt decl) = cons (fn () => report_decl Markup.ML_open loc decl)
    2.30        | report loc (PolyML.PTstructureAt decl) =
    2.31 @@ -112,11 +108,12 @@
    2.32  
    2.33      fun message {message = msg, hard, location = loc, context = _} =
    2.34        let
    2.35 +        val pos = position_of loc;
    2.36          val txt =
    2.37 -          Markup.markup Markup.no_report
    2.38 -            ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
    2.39 +          (Position.is_reported pos ? Markup.markup Markup.no_report)
    2.40 +            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
    2.41            Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
    2.42 -          Position.reported_text (offset_position_of loc)  Markup.report "";
    2.43 +          Position.reported_text pos Markup.report "";
    2.44        in if hard then err txt else warn txt end;
    2.45  
    2.46