1.1 --- a/src/Pure/General/position.ML	Fri Sep 17 15:51:11 2010 +0200
     1.2 +++ b/src/Pure/General/position.ML	Fri Sep 17 17:09:31 2010 +0200
     1.3 @@ -27,7 +27,8 @@
     1.4    val of_properties: Properties.T -> T
     1.5    val properties_of: T -> Properties.T
     1.6    val default_properties: T -> Properties.T -> Properties.T
     1.7 -  val report_markup: T -> Markup.T
     1.8 +  val markup: T -> Markup.T -> Markup.T
     1.9 +  val reported_text: Markup.T -> T -> string -> string
    1.10    val report_text: Markup.T -> T -> string -> unit
    1.11    val report: Markup.T -> T -> unit
    1.12    val str_of: T -> string
    1.13 @@ -126,12 +127,16 @@
    1.14    if exists (member (op =) Markup.position_properties o #1) props then props
    1.15    else properties_of default @ props;
    1.16  
    1.17 -fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
    1.18 +val markup = Markup.properties o properties_of;
    1.19  
    1.20 -fun report_text markup (pos as Pos (count, _)) txt =
    1.21 -  if invalid_count count then ()
    1.22 -  else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
    1.23  
    1.24 +(* reports *)
    1.25 +
    1.26 +fun reported_text m (pos as Pos (count, _)) txt =
    1.27 +  if invalid_count count then ""
    1.28 +  else Markup.markup (markup pos m) txt;
    1.29 +
    1.30 +fun report_text markup pos txt = Output.report (reported_text markup pos txt);
    1.31  fun report markup pos = report_text markup pos "";
    1.32  
    1.33  

     2.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 15:51:11 2010 +0200
     2.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 17:09:31 2010 +0200
     2.3 @@ -49,7 +49,7 @@
     2.4  
     2.5      fun report_decl markup loc decl =
     2.6        report_text Markup.ML_ref (offset_position_of loc)
     2.7 -        (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
     2.8 +        (Markup.markup (Position.markup (position_of decl) markup) "");
     2.9      fun report loc (PolyML.PTtype types) =
    2.10            PolyML.NameSpace.displayTypeExpression (types, depth, space)
    2.11            |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    2.12 @@ -124,7 +124,7 @@
    2.13            Markup.markup Markup.no_report
    2.14              ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
    2.15            Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
    2.16 -          Markup.markup (Position.report_markup (offset_position_of loc)) "";
    2.17 +          Position.reported_text Markup.report (offset_position_of loc) "";
    2.18        in if hard then err txt else warn txt end;
    2.19  
    2.20  

     3.1 --- a/src/Pure/context_position.ML	Fri Sep 17 15:51:11 2010 +0200
     3.2 +++ b/src/Pure/context_position.ML	Fri Sep 17 17:09:31 2010 +0200
     3.3 @@ -10,6 +10,7 @@
     3.4    val set_visible: bool -> Proof.context -> Proof.context
     3.5    val restore_visible: Proof.context -> Proof.context -> Proof.context
     3.6    val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
     3.7 +  val reported_text: Proof.context -> Markup.T -> Position.T -> string -> string
     3.8    val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
     3.9    val report: Proof.context -> Markup.T -> Position.T -> unit
    3.10  end;
    3.11 @@ -29,9 +30,10 @@
    3.12  
    3.13  fun if_visible ctxt f x = if is_visible ctxt then f x else ();
    3.14  
    3.15 -fun report_text ctxt markup pos txt =
    3.16 -  if is_visible ctxt then Position.report_text markup pos txt else ();
    3.17 +fun reported_text ctxt markup pos txt =
    3.18 +  if is_visible ctxt then Position.reported_text markup pos txt else "";
    3.19  
    3.20 +fun report_text ctxt markup pos txt = Output.report (reported_text ctxt markup pos txt);
    3.21  fun report ctxt markup pos = report_text ctxt markup pos "";
    3.22  
    3.23  end;