1.1 --- a/src/Pure/Isar/class.ML Sun Apr 01 19:07:32 2012 +0200
1.2 +++ b/src/Pure/Isar/class.ML Sun Apr 01 20:36:33 2012 +0200
1.3 @@ -552,8 +552,7 @@
1.4 |> synchronize_inst_syntax
1.5 |> Local_Theory.init naming
1.6 {define = Generic_Target.define foundation,
1.7 - notes = Generic_Target.notes
1.8 - (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
1.9 + notes = Generic_Target.notes Generic_Target.theory_notes,
1.10 abbrev = Generic_Target.abbrev
1.11 (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
1.12 Generic_Target.theory_abbrev prmode ((b, mx), t)),
2.1 --- a/src/Pure/Isar/generic_target.ML Sun Apr 01 19:07:32 2012 +0200
2.2 +++ b/src/Pure/Isar/generic_target.ML Sun Apr 01 20:36:33 2012 +0200
2.3 @@ -11,22 +11,26 @@
2.4 term list * term list -> local_theory -> (term * thm) * local_theory) ->
2.5 bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
2.6 (term * (string * thm)) * local_theory
2.7 - val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
2.8 + val notes:
2.9 + (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
2.10 (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
2.11 string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
2.12 (string * thm list) list * local_theory
2.13 + val locale_notes: string -> string ->
2.14 + (Attrib.binding * (thm list * Args.src list) list) list ->
2.15 + (Attrib.binding * (thm list * Args.src list) list) list ->
2.16 + local_theory -> local_theory
2.17 val abbrev: (string * bool -> binding * mixfix -> term * term ->
2.18 term list -> local_theory -> local_theory) ->
2.19 - string * bool -> (binding * mixfix) * term -> local_theory ->
2.20 - (term * term) * local_theory
2.21 -
2.22 + string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
2.23 val background_declaration: declaration -> local_theory -> local_theory
2.24 val standard_declaration: declaration -> local_theory -> local_theory
2.25 val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
2.26 -
2.27 val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
2.28 term list * term list -> local_theory -> (term * thm) * local_theory
2.29 - val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
2.30 + val theory_notes: string ->
2.31 + (Attrib.binding * (thm list * Args.src list) list) list ->
2.32 + (Attrib.binding * (thm list * Args.src list) list) list ->
2.33 local_theory -> local_theory
2.34 val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
2.35 end
2.36 @@ -96,6 +100,8 @@
2.37
2.38 (* notes *)
2.39
2.40 +local
2.41 +
2.42 fun import_export_proof ctxt (name, raw_th) =
2.43 let
2.44 val thy = Proof_Context.theory_of ctxt;
2.45 @@ -140,6 +146,11 @@
2.46
2.47 in (result'', result) end;
2.48
2.49 +fun standard_facts lthy ctxt =
2.50 + Element.transform_facts (Local_Theory.standard_morphism lthy ctxt);
2.51 +
2.52 +in
2.53 +
2.54 fun notes target_notes kind facts lthy =
2.55 let
2.56 val facts' = facts
2.57 @@ -150,10 +161,23 @@
2.58 val global_facts = Global_Theory.map_facts #2 facts';
2.59 in
2.60 lthy
2.61 - |> target_notes kind global_facts local_facts
2.62 + |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
2.63 |> Attrib.local_notes kind local_facts
2.64 end;
2.65
2.66 +fun locale_notes locale kind global_facts local_facts =
2.67 + Local_Theory.background_theory
2.68 + (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
2.69 + (fn lthy => lthy |>
2.70 + Local_Theory.target (fn ctxt => ctxt |>
2.71 + Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
2.72 + (fn lthy => lthy |>
2.73 + Local_Theory.map_contexts (fn level => fn ctxt =>
2.74 + if level = 0 orelse level = Local_Theory.level lthy then ctxt
2.75 + else ctxt |> Attrib.local_notes kind (standard_facts lthy ctxt local_facts) |> snd));
2.76 +
2.77 +end;
2.78 +
2.79
2.80 (* abbrev *)
2.81
2.82 @@ -214,9 +238,13 @@
2.83 (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
2.84 in ((lhs, def), lthy3) end;
2.85
2.86 -fun theory_notes kind global_facts =
2.87 +fun theory_notes kind global_facts local_facts =
2.88 Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
2.89 - Local_Theory.target (Attrib.local_notes kind global_facts #> snd);
2.90 + (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
2.91 + if level = Local_Theory.level lthy then ctxt
2.92 + else
2.93 + ctxt |> Attrib.local_notes kind
2.94 + (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
2.95
2.96 fun theory_abbrev prmode ((b, mx), t) =
2.97 Local_Theory.background_theory
3.1 --- a/src/Pure/Isar/named_target.ML Sun Apr 01 19:07:32 2012 +0200
3.2 +++ b/src/Pure/Isar/named_target.ML Sun Apr 01 20:36:33 2012 +0200
3.3 @@ -101,21 +101,9 @@
3.4
3.5 (* notes *)
3.6
3.7 -fun locale_notes locale kind global_facts local_facts lthy =
3.8 - let
3.9 - val global_facts' = Attrib.map_facts (K []) global_facts;
3.10 - val local_facts' = local_facts
3.11 - |> Attrib.partial_evaluation lthy
3.12 - |> Element.transform_facts (Local_Theory.target_morphism lthy);
3.13 - in
3.14 - lthy
3.15 - |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
3.16 - |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
3.17 - end;
3.18 -
3.19 fun target_notes (Target {target, is_locale, ...}) =
3.20 - if is_locale then locale_notes target
3.21 - else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
3.22 + if is_locale then Generic_Target.locale_notes target
3.23 + else Generic_Target.theory_notes;
3.24
3.25
3.26 (* abbrev *)
3.27 @@ -145,8 +133,9 @@
3.28 lthy
3.29 |> pervasive ? Generic_Target.background_declaration decl
3.30 |> Generic_Target.locale_declaration target syntax decl
3.31 - |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt => ctxt |>
3.32 - level > 0 ? Context.proof_map (Local_Theory.standard_form lthy' ctxt decl)));
3.33 + |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt =>
3.34 + if level = 0 then ctxt
3.35 + else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt));
3.36
3.37
3.38 (* pretty *)
4.1 --- a/src/Pure/Isar/overloading.ML Sun Apr 01 19:07:32 2012 +0200
4.2 +++ b/src/Pure/Isar/overloading.ML Sun Apr 01 20:36:33 2012 +0200
4.3 @@ -203,8 +203,7 @@
4.4 |> synchronize_syntax
4.5 |> Local_Theory.init naming
4.6 {define = Generic_Target.define foundation,
4.7 - notes = Generic_Target.notes
4.8 - (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
4.9 + notes = Generic_Target.notes Generic_Target.theory_notes,
4.10 abbrev = Generic_Target.abbrev
4.11 (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
4.12 Generic_Target.theory_abbrev prmode ((b, mx), t)),