tuned signature of (Context_)Position.report variants;
authorwenzelm
Fri Sep 17 20:18:27 2010 +0200 (2010-09-17)
changeset 39507839873937ddd
parent 39506 cf61ec140c4d
child 39508 dfacdb01e1ec
tuned signature of (Context_)Position.report variants;
src/Pure/General/antiquote.ML
src/Pure/General/position.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_compiler_polyml-5.3.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_lex.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/thy_output.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/context_position.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Fri Sep 17 17:31:20 2010 +0200
     1.2 +++ b/src/Pure/General/antiquote.ML	Fri Sep 17 20:18:27 2010 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4  
     1.5  (* report *)
     1.6  
     1.7 -val report_antiq = Position.report Markup.antiq;
     1.8 +fun report_antiq pos = Position.report pos Markup.antiq;
     1.9  
    1.10  fun report report_text (Text x) = report_text x
    1.11    | report _ (Antiq (_, (pos, _))) = report_antiq pos
     2.1 --- a/src/Pure/General/position.ML	Fri Sep 17 17:31:20 2010 +0200
     2.2 +++ b/src/Pure/General/position.ML	Fri Sep 17 20:18:27 2010 +0200
     2.3 @@ -28,9 +28,9 @@
     2.4    val properties_of: T -> Properties.T
     2.5    val default_properties: T -> Properties.T -> Properties.T
     2.6    val markup: T -> Markup.T -> Markup.T
     2.7 -  val reported_text: Markup.T -> T -> string -> string
     2.8 -  val report_text: Markup.T -> T -> string -> unit
     2.9 -  val report: Markup.T -> T -> unit
    2.10 +  val reported_text: T -> Markup.T -> string -> string
    2.11 +  val report_text: T -> Markup.T -> string -> unit
    2.12 +  val report: T -> Markup.T -> unit
    2.13    val str_of: T -> string
    2.14    type range = T * T
    2.15    val no_range: range
    2.16 @@ -132,12 +132,12 @@
    2.17  
    2.18  (* reports *)
    2.19  
    2.20 -fun reported_text m (pos as Pos (count, _)) txt =
    2.21 +fun reported_text (pos as Pos (count, _)) m txt =
    2.22    if invalid_count count then ""
    2.23    else Markup.markup (markup pos m) txt;
    2.24  
    2.25 -fun report_text markup pos txt = Output.report (reported_text markup pos txt);
    2.26 -fun report markup pos = report_text markup pos "";
    2.27 +fun report_text pos markup txt = Output.report (reported_text pos markup txt);
    2.28 +fun report pos markup = report_text pos markup "";
    2.29  
    2.30  
    2.31  (* str_of *)
     3.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 17 17:31:20 2010 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 17 20:18:27 2010 +0200
     3.3 @@ -108,7 +108,7 @@
     3.4        let val ((name, _), pos) = Args.dest_src src in
     3.5          (case Symtab.lookup attrs name of
     3.6            NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
     3.7 -        | SOME (att, _) => (Position.report (Markup.attribute name) pos; att src))
     3.8 +        | SOME (att, _) => (Position.report pos (Markup.attribute name); att src))
     3.9        end;
    3.10    in attr end;
    3.11  
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Sep 17 17:31:20 2010 +0200
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Sep 17 20:18:27 2010 +0200
     4.3 @@ -494,7 +494,7 @@
     4.4  (* markup commands *)
     4.5  
     4.6  fun check_text (txt, pos) state =
     4.7 - (Position.report Markup.doc_source pos;
     4.8 + (Position.report pos Markup.doc_source;
     4.9    ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
    4.10  
    4.11  fun header_markup txt = Toplevel.keep (fn state =>
     5.1 --- a/src/Pure/Isar/method.ML	Fri Sep 17 17:31:20 2010 +0200
     5.2 +++ b/src/Pure/Isar/method.ML	Fri Sep 17 20:18:27 2010 +0200
     5.3 @@ -358,7 +358,7 @@
     5.4        let val ((name, _), pos) = Args.dest_src src in
     5.5          (case Symtab.lookup meths name of
     5.6            NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
     5.7 -        | SOME (mth, _) => (Position.report (Markup.method name) pos; mth src))
     5.8 +        | SOME (mth, _) => (Position.report pos (Markup.method name); mth src))
     5.9        end;
    5.10    in meth end;
    5.11  
     6.1 --- a/src/Pure/Isar/proof_context.ML	Fri Sep 17 17:31:20 2010 +0200
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Sep 17 20:18:27 2010 +0200
     6.3 @@ -333,7 +333,7 @@
     6.4      val (syms, pos) = Syntax.read_token text;
     6.5      val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
     6.6        handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
     6.7 -    val _ = Context_Position.report ctxt (Markup.tclass c) pos;
     6.8 +    val _ = Context_Position.report ctxt pos (Markup.tclass c);
     6.9    in c end;
    6.10  
    6.11  
    6.12 @@ -467,7 +467,7 @@
    6.13      val _ =
    6.14        if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
    6.15        else ();
    6.16 -    val _ = Context_Position.report ctxt (Markup.const d) pos;
    6.17 +    val _ = Context_Position.report ctxt pos (Markup.const d);
    6.18    in t end;
    6.19  
    6.20  in
    6.21 @@ -478,13 +478,13 @@
    6.22      val (c, pos) = token_content text;
    6.23    in
    6.24      if Syntax.is_tid c then
    6.25 -     (Context_Position.report ctxt Markup.tfree pos;
    6.26 +     (Context_Position.report ctxt pos Markup.tfree;
    6.27        TFree (c, default_sort ctxt (c, ~1)))
    6.28      else
    6.29        let
    6.30          val d = Type.intern_type tsig c;
    6.31          val decl = Type.the_decl tsig d;
    6.32 -        val _ = Context_Position.report ctxt (Markup.tycon d) pos;
    6.33 +        val _ = Context_Position.report ctxt pos (Markup.tycon d);
    6.34          fun err () = error ("Bad type name: " ^ quote d);
    6.35          val args =
    6.36            (case decl of
    6.37 @@ -509,8 +509,8 @@
    6.38    in
    6.39      (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
    6.40        (SOME x, false) =>
    6.41 -        (Context_Position.report ctxt (Markup.name x
    6.42 -            (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
    6.43 +        (Context_Position.report ctxt pos
    6.44 +            (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
    6.45            Free (x, infer_type ctxt (x, ty)))
    6.46      | _ => prep_const_proper ctxt strict (c, pos))
    6.47    end;
    6.48 @@ -735,7 +735,7 @@
    6.49  
    6.50  fun parse_failed ctxt pos msg kind =
    6.51    cat_error msg ("Failed to parse " ^ kind ^
    6.52 -    Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos ""));
    6.53 +    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
    6.54  
    6.55  fun parse_sort ctxt text =
    6.56    let
    6.57 @@ -979,7 +979,8 @@
    6.58            if name = "" then [Thm.transfer thy Drule.dummy_thm]
    6.59            else
    6.60              (case Facts.lookup (Context.Proof ctxt) local_facts name of
    6.61 -              SOME (_, ths) => (Context_Position.report ctxt (Markup.local_fact name) pos;
    6.62 +              SOME (_, ths) =>
    6.63 +               (Context_Position.report ctxt pos (Markup.local_fact name);
    6.64                  map (Thm.transfer thy) (Facts.select thmref ths))
    6.65              | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
    6.66        in pick name thms end;
    6.67 @@ -1009,7 +1010,7 @@
    6.68    let
    6.69      val pos = Binding.pos_of b;
    6.70      val name = full_name ctxt b;
    6.71 -    val _ = Context_Position.report ctxt (Markup.local_fact_decl name) pos;
    6.72 +    val _ = Context_Position.report ctxt pos (Markup.local_fact_decl name);
    6.73  
    6.74      val facts = PureThy.name_thmss false name raw_facts;
    6.75      fun app (th, attrs) x =
    6.76 @@ -1188,7 +1189,7 @@
    6.77        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    6.78        |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
    6.79      val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
    6.80 -      Context_Position.report ctxt (Markup.fixed_decl x') (Binding.pos_of b));
    6.81 +      Context_Position.report ctxt (Binding.pos_of b) (Markup.fixed_decl x'));
    6.82    in (xs', ctxt'') end;
    6.83  
    6.84  
     7.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 17:31:20 2010 +0200
     7.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 20:18:27 2010 +0200
     7.3 @@ -48,12 +48,12 @@
     7.4        | _ => Position.report_text);
     7.5  
     7.6      fun report_decl markup loc decl =
     7.7 -      report_text Markup.ML_ref (offset_position_of loc)
     7.8 +      report_text (offset_position_of loc) Markup.ML_ref
     7.9          (Markup.markup (Position.markup (position_of decl) markup) "");
    7.10      fun report loc (PolyML.PTtype types) =
    7.11            PolyML.NameSpace.displayTypeExpression (types, depth, space)
    7.12            |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    7.13 -          |> report_text Markup.ML_typing (offset_position_of loc)
    7.14 +          |> report_text (offset_position_of loc) Markup.ML_typing
    7.15        | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
    7.16        | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
    7.17        | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
    7.18 @@ -124,7 +124,7 @@
    7.19            Markup.markup Markup.no_report
    7.20              ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
    7.21            Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
    7.22 -          Position.reported_text Markup.report (offset_position_of loc) "";
    7.23 +          Position.reported_text (offset_position_of loc)  Markup.report "";
    7.24        in if hard then err txt else warn txt end;
    7.25  
    7.26  
     8.1 --- a/src/Pure/ML/ml_context.ML	Fri Sep 17 17:31:20 2010 +0200
     8.2 +++ b/src/Pure/ML/ml_context.ML	Fri Sep 17 20:18:27 2010 +0200
     8.3 @@ -118,7 +118,8 @@
     8.4    let val ((name, _), pos) = Args.dest_src src in
     8.5      (case Symtab.lookup (! global_parsers) name of
     8.6        NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
     8.7 -    | SOME scan => (Context_Position.report ctxt (Markup.ML_antiq name) pos;
     8.8 +    | SOME scan =>
     8.9 +       (Context_Position.report ctxt pos (Markup.ML_antiq name);
    8.10          Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
    8.11    end;
    8.12  
     9.1 --- a/src/Pure/ML/ml_lex.ML	Fri Sep 17 17:31:20 2010 +0200
     9.2 +++ b/src/Pure/ML/ml_lex.ML	Fri Sep 17 20:18:27 2010 +0200
     9.3 @@ -112,7 +112,7 @@
     9.4  
     9.5  in
     9.6  
     9.7 -fun report_token (Token ((pos, _), (kind, x))) = Position.report (token_markup kind x) pos;
     9.8 +fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
     9.9  
    9.10  end;
    9.11  
    9.12 @@ -265,7 +265,7 @@
    9.13  
    9.14  fun read pos txt =
    9.15    let
    9.16 -    val _ = Position.report Markup.ML_source pos;
    9.17 +    val _ = Position.report pos Markup.ML_source;
    9.18      val syms = Symbol_Pos.explode (txt, pos);
    9.19      val termination =
    9.20        if null syms then []
    10.1 --- a/src/Pure/Syntax/lexicon.ML	Fri Sep 17 17:31:20 2010 +0200
    10.2 +++ b/src/Pure/Syntax/lexicon.ML	Fri Sep 17 20:18:27 2010 +0200
    10.3 @@ -187,11 +187,11 @@
    10.4    | EOF         => Markup.empty;
    10.5  
    10.6  fun report_token ctxt (Token (kind, _, (pos, _))) =
    10.7 -  Context_Position.report ctxt (token_kind_markup kind) pos;
    10.8 +  Context_Position.report ctxt pos (token_kind_markup kind);
    10.9  
   10.10  fun report_token_range ctxt tok =
   10.11    if is_proper tok
   10.12 -  then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
   10.13 +  then Context_Position.report ctxt (pos_of_token tok) Markup.token_range
   10.14    else ();
   10.15  
   10.16  
    11.1 --- a/src/Pure/Syntax/syntax.ML	Fri Sep 17 17:31:20 2010 +0200
    11.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Sep 17 20:18:27 2010 +0200
    11.3 @@ -182,7 +182,7 @@
    11.4  fun parse_token ctxt markup str =
    11.5    let
    11.6      val (syms, pos) = read_token str;
    11.7 -    val _ = Context_Position.report ctxt markup pos;
    11.8 +    val _ = Context_Position.report ctxt pos markup;
    11.9    in (syms, pos) end;
   11.10  
   11.11  local
    12.1 --- a/src/Pure/Thy/thy_output.ML	Fri Sep 17 17:31:20 2010 +0200
    12.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Sep 17 20:18:27 2010 +0200
    12.3 @@ -103,7 +103,7 @@
    12.4      (case Symtab.lookup (! global_commands) name of
    12.5        NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
    12.6      | SOME f =>
    12.7 -       (Position.report (Markup.doc_antiq name) pos;
    12.8 +       (Position.report pos (Markup.doc_antiq name);
    12.9          (fn state => fn ctxt => f src state ctxt handle ERROR msg =>
   12.10            cat_error msg ("The error(s) above occurred in document antiquotation: " ^
   12.11              quote name ^ Position.str_of pos))))
    13.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Sep 17 17:31:20 2010 +0200
    13.2 +++ b/src/Pure/Thy/thy_syntax.ML	Fri Sep 17 20:18:27 2010 +0200
    13.3 @@ -84,7 +84,7 @@
    13.4    Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
    13.5  
    13.6  fun report_token tok =
    13.7 -  Position.report (token_markup tok) (Token.position_of tok);
    13.8 +  Position.report (Token.position_of tok) (token_markup tok);
    13.9  
   13.10  end;
   13.11  
   13.12 @@ -152,7 +152,7 @@
   13.13    Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
   13.14  
   13.15  fun report_span span =
   13.16 -  Position.report (kind_markup (span_kind span)) (Position.encode_range (span_range span));
   13.17 +  Position.report (Position.encode_range (span_range span)) (kind_markup (span_kind span));
   13.18  
   13.19  end;
   13.20  
    14.1 --- a/src/Pure/context_position.ML	Fri Sep 17 17:31:20 2010 +0200
    14.2 +++ b/src/Pure/context_position.ML	Fri Sep 17 20:18:27 2010 +0200
    14.3 @@ -10,9 +10,9 @@
    14.4    val set_visible: bool -> Proof.context -> Proof.context
    14.5    val restore_visible: Proof.context -> Proof.context -> Proof.context
    14.6    val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
    14.7 -  val reported_text: Proof.context -> Markup.T -> Position.T -> string -> string
    14.8 -  val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
    14.9 -  val report: Proof.context -> Markup.T -> Position.T -> unit
   14.10 +  val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   14.11 +  val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
   14.12 +  val report: Proof.context -> Position.T -> Markup.T -> unit
   14.13  end;
   14.14  
   14.15  structure Context_Position: CONTEXT_POSITION =
   14.16 @@ -30,10 +30,10 @@
   14.17  
   14.18  fun if_visible ctxt f x = if is_visible ctxt then f x else ();
   14.19  
   14.20 -fun reported_text ctxt markup pos txt =
   14.21 -  if is_visible ctxt then Position.reported_text markup pos txt else "";
   14.22 +fun reported_text ctxt pos markup txt =
   14.23 +  if is_visible ctxt then Position.reported_text pos markup txt else "";
   14.24  
   14.25 -fun report_text ctxt markup pos txt = Output.report (reported_text ctxt markup pos txt);
   14.26 -fun report ctxt markup pos = report_text ctxt markup pos "";
   14.27 +fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
   14.28 +fun report ctxt pos markup = report_text ctxt pos markup "";
   14.29  
   14.30  end;
    15.1 --- a/src/Pure/pure_thy.ML	Fri Sep 17 17:31:20 2010 +0200
    15.2 +++ b/src/Pure/pure_thy.ML	Fri Sep 17 20:18:27 2010 +0200
    15.3 @@ -93,7 +93,7 @@
    15.4      (case res of
    15.5        NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
    15.6      | SOME (static, ths) =>
    15.7 -        (Position.report ((if static then Markup.fact else Markup.dynamic_fact) name) pos;
    15.8 +        (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name);
    15.9           Facts.select xthmref (map (Thm.transfer thy) ths)))
   15.10    end;
   15.11  
   15.12 @@ -188,7 +188,7 @@
   15.13    let
   15.14      val pos = Binding.pos_of b;
   15.15      val name = Sign.full_name thy b;
   15.16 -    val _ = Position.report (Markup.fact_decl name) pos;
   15.17 +    val _ = Position.report pos (Markup.fact_decl name);
   15.18  
   15.19      fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
   15.20      val (thms, thy') = thy |> enter_thms
    16.1 --- a/src/Pure/sign.ML	Fri Sep 17 17:31:20 2010 +0200
    16.2 +++ b/src/Pure/sign.ML	Fri Sep 17 20:18:27 2010 +0200
    16.3 @@ -426,7 +426,7 @@
    16.4    let
    16.5      val pos = Binding.pos_of b;
    16.6      val ([const as Const (c, _)], thy') = gen_add_consts (K I) [(b, T, mx)] thy;
    16.7 -    val _ = Position.report (Markup.const_decl c) pos;
    16.8 +    val _ = Position.report pos (Markup.const_decl c);
    16.9    in (const, thy') end;
   16.10  
   16.11  end;