1.1 --- a/src/Pure/Isar/proof_context.ML Sun Mar 18 12:51:44 2012 +0100
1.2 +++ b/src/Pure/Isar/proof_context.ML Sun Mar 18 13:04:22 2012 +0100
1.3 @@ -21,11 +21,6 @@
1.4 val restore_mode: Proof.context -> Proof.context -> Proof.context
1.5 val abbrev_mode: Proof.context -> bool
1.6 val set_stmt: bool -> Proof.context -> Proof.context
1.7 - val local_naming: Name_Space.naming
1.8 - val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
1.9 - val naming_of: Proof.context -> Name_Space.naming
1.10 - val restore_naming: Proof.context -> Proof.context -> Proof.context
1.11 - val full_name: Proof.context -> binding -> string
1.12 val syntax_of: Proof.context -> Local_Syntax.T
1.13 val syn_of: Proof.context -> Syntax.syntax
1.14 val tsig_of: Proof.context -> Type.tsig
1.15 @@ -37,6 +32,10 @@
1.16 val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
1.17 val facts_of: Proof.context -> Facts.T
1.18 val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
1.19 + val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
1.20 + val naming_of: Proof.context -> Name_Space.naming
1.21 + val restore_naming: Proof.context -> Proof.context -> Proof.context
1.22 + val full_name: Proof.context -> binding -> string
1.23 val class_space: Proof.context -> Name_Space.T
1.24 val type_space: Proof.context -> Name_Space.T
1.25 val const_space: Proof.context -> Name_Space.T
1.26 @@ -141,7 +140,6 @@
1.27 Context.generic -> Context.generic
1.28 val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
1.29 Context.generic -> Context.generic
1.30 - val target_naming_of: Context.generic -> Name_Space.naming
1.31 val class_alias: binding -> class -> Proof.context -> Proof.context
1.32 val type_alias: binding -> string -> Proof.context -> Proof.context
1.33 val const_alias: binding -> string -> Proof.context -> Proof.context
1.34 @@ -192,24 +190,20 @@
1.35 datatype data =
1.36 Data of
1.37 {mode: mode, (*inner syntax mode*)
1.38 - naming: Name_Space.naming, (*local naming conventions*)
1.39 syntax: Local_Syntax.T, (*local syntax*)
1.40 tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
1.41 consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
1.42 facts: Facts.T, (*local facts*)
1.43 cases: (string * (Rule_Cases.T * bool)) list}; (*named case contexts*)
1.44
1.45 -fun make_data (mode, naming, syntax, tsig, consts, facts, cases) =
1.46 - Data {mode = mode, naming = naming, syntax = syntax,
1.47 - tsig = tsig, consts = consts, facts = facts, cases = cases};
1.48 -
1.49 -val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
1.50 +fun make_data (mode, syntax, tsig, consts, facts, cases) =
1.51 + Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
1.52
1.53 structure Data = Proof_Data
1.54 (
1.55 type T = data;
1.56 fun init thy =
1.57 - make_data (mode_default, local_naming, Local_Syntax.init thy,
1.58 + make_data (mode_default, Local_Syntax.init thy,
1.59 (Sign.tsig_of thy, Sign.tsig_of thy),
1.60 (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
1.61 );
1.62 @@ -217,39 +211,35 @@
1.63 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
1.64
1.65 fun map_data f =
1.66 - Data.map (fn Data {mode, naming, syntax, tsig, consts, facts, cases} =>
1.67 - make_data (f (mode, naming, syntax, tsig, consts, facts, cases)));
1.68 + Data.map (fn Data {mode, syntax, tsig, consts, facts, cases} =>
1.69 + make_data (f (mode, syntax, tsig, consts, facts, cases)));
1.70
1.71 -fun set_mode mode = map_data (fn (_, naming, syntax, tsig, consts, facts, cases) =>
1.72 - (mode, naming, syntax, tsig, consts, facts, cases));
1.73 +fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) =>
1.74 + (mode, syntax, tsig, consts, facts, cases));
1.75
1.76 fun map_mode f =
1.77 - map_data (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) =>
1.78 - (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsig, consts, facts, cases));
1.79 -
1.80 -fun map_naming f =
1.81 - map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
1.82 - (mode, f naming, syntax, tsig, consts, facts, cases));
1.83 + map_data (fn (Mode {stmt, pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) =>
1.84 + (make_mode (f (stmt, pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases));
1.85
1.86 fun map_syntax f =
1.87 - map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
1.88 - (mode, naming, f syntax, tsig, consts, facts, cases));
1.89 + map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
1.90 + (mode, f syntax, tsig, consts, facts, cases));
1.91
1.92 fun map_tsig f =
1.93 - map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
1.94 - (mode, naming, syntax, f tsig, consts, facts, cases));
1.95 + map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
1.96 + (mode, syntax, f tsig, consts, facts, cases));
1.97
1.98 fun map_consts f =
1.99 - map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
1.100 - (mode, naming, syntax, tsig, f consts, facts, cases));
1.101 + map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
1.102 + (mode, syntax, tsig, f consts, facts, cases));
1.103
1.104 fun map_facts f =
1.105 - map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
1.106 - (mode, naming, syntax, tsig, consts, f facts, cases));
1.107 + map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
1.108 + (mode, syntax, tsig, consts, f facts, cases));
1.109
1.110 fun map_cases f =
1.111 - map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
1.112 - (mode, naming, syntax, tsig, consts, facts, f cases));
1.113 + map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
1.114 + (mode, syntax, tsig, consts, facts, f cases));
1.115
1.116 val get_mode = #mode o rep_data;
1.117 val restore_mode = set_mode o get_mode;
1.118 @@ -258,10 +248,6 @@
1.119 fun set_stmt stmt =
1.120 map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
1.121
1.122 -val naming_of = #naming o rep_data;
1.123 -val restore_naming = map_naming o K o naming_of
1.124 -val full_name = Name_Space.full_name o naming_of;
1.125 -
1.126 val syntax_of = #syntax o rep_data;
1.127 val syn_of = Local_Syntax.syn_of o syntax_of;
1.128 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
1.129 @@ -278,6 +264,15 @@
1.130 val cases_of = #cases o rep_data;
1.131
1.132
1.133 +(* naming *)
1.134 +
1.135 +val naming_of = Name_Space.naming_of o Context.Proof;
1.136 +val map_naming = Context.proof_map o Name_Space.map_naming;
1.137 +val restore_naming = map_naming o K o naming_of;
1.138 +
1.139 +val full_name = Name_Space.full_name o naming_of;
1.140 +
1.141 +
1.142 (* name spaces *)
1.143
1.144 val class_space = Type.class_space o tsig_of;
1.145 @@ -300,7 +295,7 @@
1.146 map_tsig (fn tsig as (local_tsig, global_tsig) =>
1.147 let val thy_tsig = Sign.tsig_of thy in
1.148 if Type.eq_tsig (thy_tsig, global_tsig) then tsig
1.149 - else (Type.merge_tsig ctxt (local_tsig, thy_tsig), thy_tsig)
1.150 + else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)
1.151 end) |>
1.152 map_consts (fn consts as (local_consts, global_consts) =>
1.153 let val thy_consts = Sign.consts_of thy in
1.154 @@ -495,12 +490,13 @@
1.155
1.156 fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
1.157 let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
1.158 - in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
1.159 + in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
1.160
1.161 in
1.162
1.163 val read_arity =
1.164 prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
1.165 +
1.166 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
1.167
1.168 end;
1.169 @@ -892,7 +888,7 @@
1.170
1.171 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
1.172 | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
1.173 - (Facts.add_local ctxt do_props (naming_of ctxt) (b, ths) #> snd);
1.174 + (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
1.175
1.176 in
1.177
1.178 @@ -908,7 +904,7 @@
1.179 in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
1.180
1.181 fun put_thms do_props thms ctxt = ctxt
1.182 - |> map_naming (K local_naming)
1.183 + |> map_naming (K Name_Space.local_naming)
1.184 |> Context_Position.set_visible false
1.185 |> update_thms do_props (apfst Binding.name thms)
1.186 |> Context_Position.restore_visible ctxt
1.187 @@ -993,11 +989,6 @@
1.188 end;
1.189
1.190
1.191 -(* naming *)
1.192 -
1.193 -val target_naming_of = Context.cases Sign.naming_of naming_of;
1.194 -
1.195 -
1.196 (* aliases *)
1.197
1.198 fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
1.199 @@ -1020,7 +1011,7 @@
1.200 handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
1.201 val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
1.202 val ((lhs, rhs), consts') = consts_of ctxt
1.203 - |> Consts.abbreviate ctxt (tsig_of ctxt) (naming_of ctxt) mode (b, t);
1.204 + |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t);
1.205 in
1.206 ctxt
1.207 |> (map_consts o apfst) (K consts')