# HG changeset patch
# User wenzelm
# Date 1284747507 -7200
# Node ID 839873937ddde998db5292905743c168e7872f61
# Parent  cf61ec140c4dc51dab228fb63b937b52c22dad7d
tuned signature of (Context_)Position.report variants;

diff -r cf61ec140c4d -r 839873937ddd src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/General/antiquote.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -36,7 +36,7 @@
 
 (* report *)
 
-val report_antiq = Position.report Markup.antiq;
+fun report_antiq pos = Position.report pos Markup.antiq;
 
 fun report report_text (Text x) = report_text x
   | report _ (Antiq (_, (pos, _))) = report_antiq pos
diff -r cf61ec140c4d -r 839873937ddd src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/General/position.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -28,9 +28,9 @@
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.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 reported_text: T -> Markup.T -> string -> string
+  val report_text: T -> Markup.T -> string -> unit
+  val report: T -> Markup.T -> unit
   val str_of: T -> string
   type range = T * T
   val no_range: range
@@ -132,12 +132,12 @@
 
 (* reports *)
 
-fun reported_text m (pos as Pos (count, _)) txt =
+fun reported_text (pos as Pos (count, _)) m 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 "";
+fun report_text pos markup txt = Output.report (reported_text pos markup txt);
+fun report pos markup = report_text pos markup "";
 
 
 (* str_of *)
diff -r cf61ec140c4d -r 839873937ddd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -108,7 +108,7 @@
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup attrs name of
           NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
-        | SOME (att, _) => (Position.report (Markup.attribute name) pos; att src))
+        | SOME (att, _) => (Position.report pos (Markup.attribute name); att src))
       end;
   in attr end;
 
diff -r cf61ec140c4d -r 839873937ddd src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -494,7 +494,7 @@
 (* markup commands *)
 
 fun check_text (txt, pos) state =
- (Position.report Markup.doc_source pos;
+ (Position.report pos Markup.doc_source;
   ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
 
 fun header_markup txt = Toplevel.keep (fn state =>
diff -r cf61ec140c4d -r 839873937ddd src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/Isar/method.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -358,7 +358,7 @@
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup meths name of
           NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
-        | SOME (mth, _) => (Position.report (Markup.method name) pos; mth src))
+        | SOME (mth, _) => (Position.report pos (Markup.method name); mth src))
       end;
   in meth end;
 
diff -r cf61ec140c4d -r 839873937ddd src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -333,7 +333,7 @@
     val (syms, pos) = Syntax.read_token text;
     val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
       handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
-    val _ = Context_Position.report ctxt (Markup.tclass c) pos;
+    val _ = Context_Position.report ctxt pos (Markup.tclass c);
   in c end;
 
 
@@ -467,7 +467,7 @@
     val _ =
       if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
       else ();
-    val _ = Context_Position.report ctxt (Markup.const d) pos;
+    val _ = Context_Position.report ctxt pos (Markup.const d);
   in t end;
 
 in
@@ -478,13 +478,13 @@
     val (c, pos) = token_content text;
   in
     if Syntax.is_tid c then
-     (Context_Position.report ctxt Markup.tfree pos;
+     (Context_Position.report ctxt pos Markup.tfree;
       TFree (c, default_sort ctxt (c, ~1)))
     else
       let
         val d = Type.intern_type tsig c;
         val decl = Type.the_decl tsig d;
-        val _ = Context_Position.report ctxt (Markup.tycon d) pos;
+        val _ = Context_Position.report ctxt pos (Markup.tycon d);
         fun err () = error ("Bad type name: " ^ quote d);
         val args =
           (case decl of
@@ -509,8 +509,8 @@
   in
     (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
-        (Context_Position.report ctxt (Markup.name x
-            (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
+        (Context_Position.report ctxt pos
+            (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
           Free (x, infer_type ctxt (x, ty)))
     | _ => prep_const_proper ctxt strict (c, pos))
   end;
@@ -735,7 +735,7 @@
 
 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
-    Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos ""));
+    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
 
 fun parse_sort ctxt text =
   let
@@ -979,7 +979,8 @@
           if name = "" then [Thm.transfer thy Drule.dummy_thm]
           else
             (case Facts.lookup (Context.Proof ctxt) local_facts name of
-              SOME (_, ths) => (Context_Position.report ctxt (Markup.local_fact name) pos;
+              SOME (_, ths) =>
+               (Context_Position.report ctxt pos (Markup.local_fact name);
                 map (Thm.transfer thy) (Facts.select thmref ths))
             | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
       in pick name thms end;
@@ -1009,7 +1010,7 @@
   let
     val pos = Binding.pos_of b;
     val name = full_name ctxt b;
-    val _ = Context_Position.report ctxt (Markup.local_fact_decl name) pos;
+    val _ = Context_Position.report ctxt pos (Markup.local_fact_decl name);
 
     val facts = PureThy.name_thmss false name raw_facts;
     fun app (th, attrs) x =
@@ -1188,7 +1189,7 @@
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
       |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
     val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
-      Context_Position.report ctxt (Markup.fixed_decl x') (Binding.pos_of b));
+      Context_Position.report ctxt (Binding.pos_of b) (Markup.fixed_decl x'));
   in (xs', ctxt'') end;
 
 
diff -r cf61ec140c4d -r 839873937ddd src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -48,12 +48,12 @@
       | _ => Position.report_text);
 
     fun report_decl markup loc decl =
-      report_text Markup.ML_ref (offset_position_of loc)
+      report_text (offset_position_of loc) Markup.ML_ref
         (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
-          |> report_text Markup.ML_typing (offset_position_of loc)
+          |> report_text (offset_position_of loc) Markup.ML_typing
       | 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
@@ -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)) ^
-          Position.reported_text Markup.report (offset_position_of loc) "";
+          Position.reported_text (offset_position_of loc)  Markup.report "";
       in if hard then err txt else warn txt end;
 
 
diff -r cf61ec140c4d -r 839873937ddd src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -118,7 +118,8 @@
   let val ((name, _), pos) = Args.dest_src src in
     (case Symtab.lookup (! global_parsers) name of
       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
-    | SOME scan => (Context_Position.report ctxt (Markup.ML_antiq name) pos;
+    | SOME scan =>
+       (Context_Position.report ctxt pos (Markup.ML_antiq name);
         Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
   end;
 
diff -r cf61ec140c4d -r 839873937ddd src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -112,7 +112,7 @@
 
 in
 
-fun report_token (Token ((pos, _), (kind, x))) = Position.report (token_markup kind x) pos;
+fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
 
 end;
 
@@ -265,7 +265,7 @@
 
 fun read pos txt =
   let
-    val _ = Position.report Markup.ML_source pos;
+    val _ = Position.report pos Markup.ML_source;
     val syms = Symbol_Pos.explode (txt, pos);
     val termination =
       if null syms then []
diff -r cf61ec140c4d -r 839873937ddd src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -187,11 +187,11 @@
   | EOF         => Markup.empty;
 
 fun report_token ctxt (Token (kind, _, (pos, _))) =
-  Context_Position.report ctxt (token_kind_markup kind) pos;
+  Context_Position.report ctxt pos (token_kind_markup kind);
 
 fun report_token_range ctxt tok =
   if is_proper tok
-  then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
+  then Context_Position.report ctxt (pos_of_token tok) Markup.token_range
   else ();
 
 
diff -r cf61ec140c4d -r 839873937ddd src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -182,7 +182,7 @@
 fun parse_token ctxt markup str =
   let
     val (syms, pos) = read_token str;
-    val _ = Context_Position.report ctxt markup pos;
+    val _ = Context_Position.report ctxt pos markup;
   in (syms, pos) end;
 
 local
diff -r cf61ec140c4d -r 839873937ddd src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -103,7 +103,7 @@
     (case Symtab.lookup (! global_commands) name of
       NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
     | SOME f =>
-       (Position.report (Markup.doc_antiq name) pos;
+       (Position.report pos (Markup.doc_antiq name);
         (fn state => fn ctxt => f src state ctxt handle ERROR msg =>
           cat_error msg ("The error(s) above occurred in document antiquotation: " ^
             quote name ^ Position.str_of pos))))
diff -r cf61ec140c4d -r 839873937ddd src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -84,7 +84,7 @@
   Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
 
 fun report_token tok =
-  Position.report (token_markup tok) (Token.position_of tok);
+  Position.report (Token.position_of tok) (token_markup tok);
 
 end;
 
@@ -152,7 +152,7 @@
   Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
 
 fun report_span span =
-  Position.report (kind_markup (span_kind span)) (Position.encode_range (span_range span));
+  Position.report (Position.encode_range (span_range span)) (kind_markup (span_kind span));
 
 end;
 
diff -r cf61ec140c4d -r 839873937ddd src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/context_position.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -10,9 +10,9 @@
   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
+  val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
+  val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
+  val report: Proof.context -> Position.T -> Markup.T -> unit
 end;
 
 structure Context_Position: CONTEXT_POSITION =
@@ -30,10 +30,10 @@
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
 
-fun reported_text ctxt markup pos txt =
-  if is_visible ctxt then Position.reported_text markup pos txt else "";
+fun reported_text ctxt pos markup txt =
+  if is_visible ctxt then Position.reported_text pos markup 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 "";
+fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
+fun report ctxt pos markup = report_text ctxt pos markup "";
 
 end;
diff -r cf61ec140c4d -r 839873937ddd src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/pure_thy.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -93,7 +93,7 @@
     (case res of
       NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
     | SOME (static, ths) =>
-        (Position.report ((if static then Markup.fact else Markup.dynamic_fact) name) pos;
+        (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name);
          Facts.select xthmref (map (Thm.transfer thy) ths)))
   end;
 
@@ -188,7 +188,7 @@
   let
     val pos = Binding.pos_of b;
     val name = Sign.full_name thy b;
-    val _ = Position.report (Markup.fact_decl name) pos;
+    val _ = Position.report pos (Markup.fact_decl name);
 
     fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
     val (thms, thy') = thy |> enter_thms
diff -r cf61ec140c4d -r 839873937ddd src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/sign.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -426,7 +426,7 @@
   let
     val pos = Binding.pos_of b;
     val ([const as Const (c, _)], thy') = gen_add_consts (K I) [(b, T, mx)] thy;
-    val _ = Position.report (Markup.const_decl c) pos;
+    val _ = Position.report pos (Markup.const_decl c);
   in (const, thy') end;
 
 end;