# HG changeset patch # User haftmann # Date 1281442288 -7200 # Node ID 0e4649095739435d87107c1ad982c7c2d70cde98 # Parent 0028571ade2d32a469f05671d1c4a40d53f67475 try to uniformly follow define/note/abbrev/declaration order as close as possible diff -r 0028571ade2d -r 0e4649095739 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Tue Aug 10 14:06:38 2010 +0200 +++ b/src/Pure/Isar/local_theory.ML Tue Aug 10 14:11:28 2010 +0200 @@ -30,9 +30,6 @@ val standard_morphism: local_theory -> Proof.context -> morphism val target_morphism: local_theory -> morphism val global_morphism: local_theory -> morphism - val pretty: local_theory -> Pretty.T list - val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> - (term * term) * local_theory val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory @@ -40,8 +37,11 @@ local_theory -> (string * thm list) list * local_theory val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> local_theory -> (string * thm list) list * local_theory + val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> + (term * term) * local_theory val declaration: bool -> declaration -> local_theory -> local_theory val syntax_declaration: bool -> declaration -> local_theory -> local_theory + val pretty: local_theory -> Pretty.T list val set_defsort: sort -> local_theory -> local_theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory @@ -65,16 +65,16 @@ (* type lthy *) type operations = - {pretty: local_theory -> Pretty.T list, - abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> - (term * term) * local_theory, - define: (binding * mixfix) * (Attrib.binding * term) -> local_theory -> + {define: (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory, notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> local_theory -> (string * thm list) list * local_theory, + abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> + (term * term) * local_theory, declaration: bool -> declaration -> local_theory -> local_theory, syntax_declaration: bool -> declaration -> local_theory -> local_theory, + pretty: local_theory -> Pretty.T list, reinit: local_theory -> local_theory, exit: local_theory -> Proof.context}; diff -r 0028571ade2d -r 0e4649095739 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Tue Aug 10 14:06:38 2010 +0200 +++ b/src/Pure/Isar/theory_target.ML Tue Aug 10 14:11:28 2010 +0200 @@ -45,36 +45,6 @@ val peek = (fn Target args => args) o Data.get; -(* pretty *) - -fun pretty_thy ctxt target is_class = - let - val thy = ProofContext.theory_of ctxt; - val target_name = - [Pretty.command (if is_class then "class" else "locale"), - Pretty.str (" " ^ Locale.extern thy target)]; - val fixes = - map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); - val assumes = - map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.all_assms_of ctxt); - val elems = - (if null fixes then [] else [Element.Fixes fixes]) @ - (if null assumes then [] else [Element.Assumes assumes]); - in - if target = "" then [] - else if null elems then [Pretty.block target_name] - else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: - map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))] - end; - -fun pretty (Target {target, is_class, instantiation, overloading, ...}) ctxt = - Pretty.block [Pretty.command "theory", Pretty.brk 1, - Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: - (if not (null overloading) then [Overloading.pretty ctxt] - else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt] - else pretty_thy ctxt target is_class); - - (* generic declarations *) fun theory_declaration decl lthy = @@ -102,33 +72,6 @@ else locale_declaration target { syntax = syntax, pervasive = pervasive }; -(* notes *) - -fun theory_notes kind global_facts lthy = - let - val thy = ProofContext.theory_of lthy; - val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts; - in - lthy - |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd) - |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd) - end; - -fun locale_notes locale kind global_facts local_facts lthy = - let - val global_facts' = Attrib.map_facts (K I) global_facts; - val local_facts' = Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts; - in - lthy - |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd) - |> Local_Theory.target (Locale.add_thmss locale kind local_facts') - end - -fun notes (Target {target, is_locale, ...}) = - Generic_Target.notes (if is_locale then locale_notes target - else fn kind => fn global_facts => fn _ => theory_notes kind global_facts); - - (* consts in locales *) fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi = @@ -190,30 +133,6 @@ end; -(* abbrev *) - -fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory - (Sign.add_abbrev (#1 prmode) (b, t) #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)])); - -fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result - (Sign.add_abbrev Print_Mode.internal (b, t)) #-> (fn (lhs, _) => - locale_const_declaration ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); - -fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) - prmode (b, mx) (global_rhs, t') (extra_tfrees, xs) lthy = - let - val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx; - in if is_locale - then lthy - |> locale_abbrev ta prmode ((b, mx2), global_rhs) xs - |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t')) - else lthy - |> theory_abbrev prmode ((b, mx3), global_rhs) - end; - -fun abbrev ta = Generic_Target.abbrev (target_abbrev ta); - - (* define *) local @@ -260,6 +179,87 @@ end; +(* notes *) + +fun theory_notes kind global_facts lthy = + let + val thy = ProofContext.theory_of lthy; + val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts; + in + lthy + |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd) + |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd) + end; + +fun locale_notes locale kind global_facts local_facts lthy = + let + val global_facts' = Attrib.map_facts (K I) global_facts; + val local_facts' = Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts; + in + lthy + |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd) + |> Local_Theory.target (Locale.add_thmss locale kind local_facts') + end + +fun notes (Target {target, is_locale, ...}) = + Generic_Target.notes (if is_locale then locale_notes target + else fn kind => fn global_facts => fn _ => theory_notes kind global_facts); + + +(* abbrev *) + +fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory + (Sign.add_abbrev (#1 prmode) (b, t) #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)])); + +fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result + (Sign.add_abbrev Print_Mode.internal (b, t)) #-> (fn (lhs, _) => + locale_const_declaration ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); + +fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) + prmode (b, mx) (global_rhs, t') (extra_tfrees, xs) lthy = + let + val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx; + in if is_locale + then lthy + |> locale_abbrev ta prmode ((b, mx2), global_rhs) xs + |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t')) + else lthy + |> theory_abbrev prmode ((b, mx3), global_rhs) + end; + +fun abbrev ta = Generic_Target.abbrev (target_abbrev ta); + + +(* pretty *) + +fun pretty_thy ctxt target is_class = + let + val thy = ProofContext.theory_of ctxt; + val target_name = + [Pretty.command (if is_class then "class" else "locale"), + Pretty.str (" " ^ Locale.extern thy target)]; + val fixes = + map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); + val assumes = + map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.all_assms_of ctxt); + val elems = + (if null fixes then [] else [Element.Fixes fixes]) @ + (if null assumes then [] else [Element.Assumes assumes]); + in + if target = "" then [] + else if null elems then [Pretty.block target_name] + else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: + map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))] + end; + +fun pretty (Target {target, is_class, instantiation, overloading, ...}) ctxt = + Pretty.block [Pretty.command "theory", Pretty.brk 1, + Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: + (if not (null overloading) then [Overloading.pretty ctxt] + else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt] + else pretty_thy ctxt target is_class); + + (* init various targets *) local @@ -276,12 +276,12 @@ |> init_data ta |> Data.put ta |> Local_Theory.init NONE (Long_Name.base_name target) - {pretty = pretty ta, + {define = define ta, + notes = notes ta, abbrev = abbrev ta, - define = define ta, - notes = notes ta, declaration = fn pervasive => target_declaration ta { syntax = false, pervasive = pervasive }, syntax_declaration = fn pervasive => target_declaration ta { syntax = true, pervasive = pervasive }, + pretty = pretty ta, reinit = init_target ta o ProofContext.theory_of, exit = Local_Theory.target_of o (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation