more decisive commitment to get_free vs. the_const;
authorwenzelm
Thu Mar 06 17:37:32 2014 +0100 (2014-03-06)
changeset 55959c3b458435f4f
parent 55958 4ec984df4f45
child 55960 beef468837b1
more decisive commitment to get_free vs. the_const;
tuned;
src/Pure/General/position.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/General/position.ML	Thu Mar 06 16:33:48 2014 +0100
     1.2 +++ b/src/Pure/General/position.ML	Thu Mar 06 17:37:32 2014 +0100
     1.3 @@ -43,6 +43,7 @@
     1.4    val reports: report list -> unit
     1.5    val store_reports: report_text list Unsynchronized.ref ->
     1.6      T list -> ('a -> Markup.T list) -> 'a -> unit
     1.7 +  val append_reports: report_text list Unsynchronized.ref -> report list -> unit
     1.8    val here: T -> string
     1.9    val here_list: T list -> string
    1.10    type range = T * T
    1.11 @@ -182,6 +183,9 @@
    1.12        let val ms = markup x
    1.13        in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
    1.14  
    1.15 +fun append_reports (r: report_text list Unsynchronized.ref) reports =
    1.16 +  Unsynchronized.change r (append (map (rpair "") reports));
    1.17 +
    1.18  
    1.19  (* here: inlined formal markup *)
    1.20  
     2.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 16:33:48 2014 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 17:37:32 2014 +0100
     2.3 @@ -73,7 +73,7 @@
     2.4    val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
     2.5    val consts_completion_message: Proof.context -> xstring * Position.T list -> string
     2.6    val check_const: Proof.context -> {proper: bool, strict: bool} ->
     2.7 -    xstring * Position.T -> term * Position.report list
     2.8 +    xstring * Position.T list -> term * Position.report list
     2.9    val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
    2.10    val read_arity: Proof.context -> xstring * string list * string -> arity
    2.11    val cert_arity: Proof.context -> arity -> arity
    2.12 @@ -476,31 +476,31 @@
    2.13    |> implode
    2.14    |> Markup.markup_report;
    2.15  
    2.16 -fun check_const ctxt {proper, strict} (c, pos) =
    2.17 +fun check_const ctxt {proper, strict} (c, ps) =
    2.18    let
    2.19      val _ =
    2.20 -      Name.reject_internal (c, [pos]) handle ERROR msg =>
    2.21 -        error (msg ^ consts_completion_message ctxt (c, [pos]));
    2.22 -    fun err msg = error (msg ^ Position.here pos);
    2.23 +      Name.reject_internal (c, ps) handle ERROR msg =>
    2.24 +        error (msg ^ consts_completion_message ctxt (c, ps));
    2.25 +    fun err msg = error (msg ^ Position.here_list ps);
    2.26      val consts = consts_of ctxt;
    2.27      val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
    2.28      val (t, reports) =
    2.29        (case (fixed, Variable.lookup_const ctxt c) of
    2.30          (SOME x, NONE) =>
    2.31            let
    2.32 -            val reports =
    2.33 -              if Context_Position.is_reported ctxt pos then
    2.34 -                [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
    2.35 -              else [];
    2.36 +            val reports = ps
    2.37 +              |> filter (Context_Position.is_reported ctxt)
    2.38 +              |> map (fn pos =>
    2.39 +                (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)));
    2.40            in (Free (x, infer_type ctxt (x, dummyT)), reports) end
    2.41        | (_, SOME d) =>
    2.42            let
    2.43              val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
    2.44 -            val reports =
    2.45 -              if Context_Position.is_reported ctxt pos
    2.46 -              then [(pos, Name_Space.markup (Consts.space_of consts) d)] else [];
    2.47 +            val reports = ps
    2.48 +              |> filter (Context_Position.is_reported ctxt)
    2.49 +              |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
    2.50            in (Const (d, T), reports) end
    2.51 -      | _ => Consts.check_const (Context.Proof ctxt) consts (c, [pos]));
    2.52 +      | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps));
    2.53      val _ =
    2.54        (case (strict, t) of
    2.55          (true, Const (d, _)) =>
    2.56 @@ -510,8 +510,8 @@
    2.57  
    2.58  fun read_const ctxt flags text =
    2.59    let
    2.60 -    val (t, reports) =
    2.61 -      check_const ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
    2.62 +    val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
    2.63 +    val (t, reports) = check_const ctxt flags (xname, [pos]);
    2.64      val _ = Position.reports reports;
    2.65    in t end;
    2.66  
     3.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 16:33:48 2014 +0100
     3.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 17:37:32 2014 +0100
     3.3 @@ -140,6 +140,7 @@
     3.4    let
     3.5      val reports = Unsynchronized.ref ([]: Position.report_text list);
     3.6      fun report pos = Position.store_reports reports [pos];
     3.7 +    val append_reports = Position.append_reports reports;
     3.8  
     3.9      fun trans a args =
    3.10        (case trf a of
    3.11 @@ -164,7 +165,7 @@
    3.12            let
    3.13              val pos = Lexicon.pos_of_token tok;
    3.14              val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos);
    3.15 -            val _ = Unsynchronized.change reports (append (map (rpair "") rs));
    3.16 +            val _ = append_reports rs;
    3.17            in [Ast.Constant (Lexicon.mark_class c)] end
    3.18        | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
    3.19            let
    3.20 @@ -172,7 +173,7 @@
    3.21              val (Type (c, _), rs) =
    3.22                Proof_Context.check_type_name ctxt {proper = true, strict = false}
    3.23                  (Lexicon.str_of_token tok, pos);
    3.24 -            val _ = Unsynchronized.change reports (append (map (rpair "") rs));
    3.25 +            val _ = append_reports rs;
    3.26            in [Ast.Constant (Lexicon.mark_type c)] end
    3.27        | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
    3.28        | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
    3.29 @@ -221,22 +222,23 @@
    3.30  
    3.31  (* decode_term -- transform parse tree into raw term *)
    3.32  
    3.33 -fun decode_const ctxt c =
    3.34 +fun decode_const ctxt (c, ps) =
    3.35    let
    3.36 -    val (Const (c', _), _) =
    3.37 -      Proof_Context.check_const ctxt {proper = true, strict = false} (c, Position.none);
    3.38 -  in c' end;
    3.39 +    val (Const (c', _), reports) =
    3.40 +      Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
    3.41 +  in (c', reports) end;
    3.42  
    3.43  fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
    3.44    | decode_term ctxt (reports0, Exn.Res tm) =
    3.45        let
    3.46 -        fun get_const c =
    3.47 -          (true, decode_const ctxt c) handle ERROR _ =>
    3.48 -            (false, Consts.intern (Proof_Context.consts_of ctxt) c);
    3.49 +        val reports = Unsynchronized.ref reports0;
    3.50 +        fun report ps = Position.store_reports reports ps;
    3.51 +        val append_reports = Position.append_reports reports;
    3.52 +
    3.53          fun get_free x =
    3.54            let
    3.55              val fixed = Variable.lookup_fixed ctxt x;
    3.56 -            val is_const = can (decode_const ctxt) x orelse Long_Name.is_qualified x;
    3.57 +            val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
    3.58              val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
    3.59            in
    3.60              if Variable.is_const ctxt x then NONE
    3.61 @@ -245,8 +247,11 @@
    3.62              else NONE
    3.63            end;
    3.64  
    3.65 -        val reports = Unsynchronized.ref reports0;
    3.66 -        fun report ps = Position.store_reports reports ps;
    3.67 +        fun the_const (a, ps) =
    3.68 +          let
    3.69 +            val (c, rs) = decode_const ctxt (a, ps);
    3.70 +            val _ = append_reports rs;
    3.71 +          in c end;
    3.72  
    3.73          fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
    3.74                (case Term_Position.decode_position typ of
    3.75 @@ -269,20 +274,15 @@
    3.76                    let
    3.77                      val c =
    3.78                        (case try Lexicon.unmark_const a of
    3.79 -                        SOME c => c
    3.80 -                      | NONE => snd (get_const a));
    3.81 -                    val _ = report ps (markup_const ctxt) c;
    3.82 +                        SOME c => (report ps (markup_const ctxt) c; c)
    3.83 +                      | NONE => the_const (a, ps));
    3.84                    in Const (c, T) end)
    3.85            | decode ps _ _ (Free (a, T)) =
    3.86                ((Name.reject_internal (a, ps) handle ERROR msg =>
    3.87                    error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
    3.88 -                (case (get_free a, get_const a) of
    3.89 -                  (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
    3.90 -                | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
    3.91 -                | (_, (false, c)) =>
    3.92 -                    if Long_Name.is_qualified c
    3.93 -                    then (report ps (markup_const ctxt) c; Const (c, T))
    3.94 -                    else (report ps (markup_free ctxt) c; Free (c, T))))
    3.95 +                (case get_free a of
    3.96 +                  SOME x => (report ps (markup_free ctxt) x; Free (x, T))
    3.97 +                | NONE => Const (the_const (a, ps), T)))
    3.98            | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
    3.99            | decode ps _ bs (t as Bound i) =
   3.100                (case try (nth bs) i of
   3.101 @@ -813,7 +813,7 @@
   3.102  
   3.103  fun const_ast_tr intern ctxt [Ast.Variable c] =
   3.104        let
   3.105 -        val c' = decode_const ctxt c;
   3.106 +        val (c', _) = decode_const ctxt (c, []);
   3.107          val d = if intern then Lexicon.mark_const c' else c;
   3.108        in Ast.Constant d end
   3.109    | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =