# HG changeset patch
# User wenzelm
# Date 1284736171 -7200
# Node ID 4c2547af5909a3a5bb7bc65491a37c9fa9fb8815
# Parent  1c294d150ded9fea8ee467a7c871ce0156e27ba9
simplified/clarified (Context_)Position.markup/reported_text;

diff -r 1c294d150ded -r 4c2547af5909 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri Sep 17 15:51:11 2010 +0200
+++ b/src/Pure/General/position.ML	Fri Sep 17 17:09:31 2010 +0200
@@ -27,7 +27,8 @@
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
-  val report_markup: T -> Markup.T
+  val markup: T -> Markup.T -> Markup.T
+  val reported_text: Markup.T -> T -> string -> string
   val report_text: Markup.T -> T -> string -> unit
   val report: Markup.T -> T -> unit
   val str_of: T -> string
@@ -126,12 +127,16 @@
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
 
-fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
+val markup = Markup.properties o properties_of;
+
+
+(* reports *)
 
-fun report_text markup (pos as Pos (count, _)) txt =
-  if invalid_count count then ()
-  else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
+fun reported_text m (pos as Pos (count, _)) txt =
+  if invalid_count count then ""
+  else Markup.markup (markup pos m) txt;
 
+fun report_text markup pos txt = Output.report (reported_text markup pos txt);
 fun report markup pos = report_text markup pos "";
 
 
diff -r 1c294d150ded -r 4c2547af5909 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 15:51:11 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 17:09:31 2010 +0200
@@ -49,7 +49,7 @@
 
     fun report_decl markup loc decl =
       report_text Markup.ML_ref (offset_position_of loc)
-        (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
+        (Markup.markup (Position.markup (position_of decl) markup) "");
     fun report loc (PolyML.PTtype types) =
           PolyML.NameSpace.displayTypeExpression (types, depth, space)
           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
@@ -124,7 +124,7 @@
           Markup.markup Markup.no_report
             ((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 (offset_position_of loc)) "";
+          Position.reported_text Markup.report (offset_position_of loc) "";
       in if hard then err txt else warn txt end;
 
 
diff -r 1c294d150ded -r 4c2547af5909 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Fri Sep 17 15:51:11 2010 +0200
+++ b/src/Pure/context_position.ML	Fri Sep 17 17:09:31 2010 +0200
@@ -10,6 +10,7 @@
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
+  val reported_text: Proof.context -> Markup.T -> Position.T -> string -> string
   val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
   val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
@@ -29,9 +30,10 @@
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
 
-fun report_text ctxt markup pos txt =
-  if is_visible ctxt then Position.report_text markup pos txt else ();
+fun reported_text ctxt markup pos txt =
+  if is_visible ctxt then Position.reported_text markup pos txt else "";
 
+fun report_text ctxt markup pos txt = Output.report (reported_text ctxt markup pos txt);
 fun report ctxt markup pos = report_text ctxt markup pos "";
 
 end;