# HG changeset patch # User wenzelm # Date 1357398982 -3600 # Node ID f310d1735d935246a8f819222929c21e66e0bb0e # Parent 07dfdf72ab757c47253d6101602f4991ca5b51f5 tuned -- less indirection; diff -r 07dfdf72ab75 -r f310d1735d93 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Jan 05 11:24:09 2013 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sat Jan 05 16:16:22 2013 +0100 @@ -16,7 +16,6 @@ val translations: (xstring * string) Syntax.trrule list -> theory -> theory val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory - val add_axioms: (Attrib.binding * string) list -> theory -> theory val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory val declaration: {syntax: bool, pervasive: bool} -> Symbol_Pos.text * Position.T -> local_theory -> local_theory @@ -42,32 +41,13 @@ val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm} val display_drafts: string list -> Toplevel.transition -> Toplevel.transition val print_drafts: string list -> Toplevel.transition -> Toplevel.transition - val print_context: Toplevel.transition -> Toplevel.transition - val print_theory: bool -> Toplevel.transition -> Toplevel.transition - val print_syntax: Toplevel.transition -> Toplevel.transition - val print_abbrevs: Toplevel.transition -> Toplevel.transition - val print_facts: Toplevel.transition -> Toplevel.transition - val print_configs: Toplevel.transition -> Toplevel.transition val print_theorems: bool -> Toplevel.transition -> Toplevel.transition - val print_locales: Toplevel.transition -> Toplevel.transition - val print_locale: bool * (xstring * Position.T) -> Toplevel.transition -> Toplevel.transition - val print_registrations: xstring * Position.T -> Toplevel.transition -> Toplevel.transition - val print_dependencies: bool * Expression.expression -> Toplevel.transition - -> Toplevel.transition - val print_attributes: Toplevel.transition -> Toplevel.transition - val print_simpset: Toplevel.transition -> Toplevel.transition - val print_rules: Toplevel.transition -> Toplevel.transition - val print_trans_rules: Toplevel.transition -> Toplevel.transition - val print_methods: Toplevel.transition -> Toplevel.transition - val print_antiquotations: Toplevel.transition -> Toplevel.transition val thy_deps: Toplevel.transition -> Toplevel.transition val locale_deps: Toplevel.transition -> Toplevel.transition val class_deps: Toplevel.transition -> Toplevel.transition val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition val unused_thms: (string list * string list option) option -> Toplevel.transition -> Toplevel.transition - val print_binds: Toplevel.transition -> Toplevel.transition - val print_cases: Toplevel.transition -> Toplevel.transition val print_stmts: string list * (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition val print_thms: string list * (Facts.ref * Attrib.src list) list @@ -187,9 +167,7 @@ in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end; -(* old-style axioms *) - -val add_axioms = fold (snd oo Specification.axiom_cmd); +(* old-style defs *) fun add_defs ((unchecked, overloaded), args) thy = thy |> @@ -328,24 +306,7 @@ in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end); -(* print parts of theory and proof context *) - -val print_context = Toplevel.keep Toplevel.print_state_context; - -fun print_theory verbose = Toplevel.unknown_theory o - Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of); - -val print_syntax = Toplevel.unknown_context o - Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of); - -val print_abbrevs = Toplevel.unknown_context o - Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of); - -val print_facts = Toplevel.unknown_context o - Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of); - -val print_configs = Toplevel.unknown_context o - Toplevel.keep (Attrib.print_configs o Toplevel.context_of); +(* print theorems *) val print_theorems_proof = Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of); @@ -359,39 +320,8 @@ fun print_theorems verbose = Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof; -val print_locales = Toplevel.unknown_theory o - Toplevel.keep (Locale.print_locales o Toplevel.theory_of); -fun print_locale (verbose, name) = Toplevel.unknown_theory o - Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) verbose name); - -fun print_registrations name = Toplevel.unknown_context o - Toplevel.keep (fn state => - Locale.print_registrations (Toplevel.context_of state) name); - -fun print_dependencies (clean, expression) = Toplevel.unknown_context o - Toplevel.keep (fn state => - Expression.print_dependencies (Toplevel.context_of state) clean expression); - -val print_attributes = Toplevel.unknown_theory o - Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); - -val print_simpset = Toplevel.unknown_context o - Toplevel.keep (fn state => - let val ctxt = Toplevel.context_of state - in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end); - -val print_rules = Toplevel.unknown_context o - Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of); - -val print_trans_rules = Toplevel.unknown_context o - Toplevel.keep (Calculation.print_rules o Toplevel.context_of); - -val print_methods = Toplevel.unknown_theory o - Toplevel.keep (Method.print_methods o Toplevel.theory_of); - -val print_antiquotations = - Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of); +(* display dependencies *) val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => let @@ -454,15 +384,6 @@ end); -(* print proof context contents *) - -val print_binds = Toplevel.unknown_context o - Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of); - -val print_cases = Toplevel.unknown_context o - Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of); - - (* print theorems, terms, types etc. *) local diff -r 07dfdf72ab75 -r f310d1735d93 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat Jan 05 11:24:09 2013 +0100 +++ b/src/Pure/Isar/isar_syn.ML Sat Jan 05 16:16:22 2013 +0100 @@ -174,7 +174,7 @@ (Scan.repeat1 Parse_Spec.spec >> (fn spec => Toplevel.theory (fn thy => (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"; - Isar_Cmd.add_axioms spec thy)))); + fold (snd oo Specification.axiom_cmd) spec thy)))); val opt_unchecked_overloaded = Scan.optional (@{keyword "("} |-- Parse.!!! @@ -775,26 +775,30 @@ val _ = Outer_Syntax.improper_command @{command_spec "print_configs"} "print configuration options" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (Attrib.print_configs o Toplevel.context_of))); val _ = - Outer_Syntax.improper_command @{command_spec "print_context"} "print theory context name" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context)); + Outer_Syntax.improper_command @{command_spec "print_context"} "print main context" + (Scan.succeed (Toplevel.no_timing o Toplevel.keep Toplevel.print_state_context)); val _ = Outer_Syntax.improper_command @{command_spec "print_theory"} "print logical theory contents (verbose!)" - (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory)); + (opt_bang >> (fn b => Toplevel.no_timing o Toplevel.unknown_theory o + Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_syntax"} "print inner syntax of context (verbose!)" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_abbrevs"} "print constant abbreviation of context" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_theorems"} @@ -804,7 +808,8 @@ val _ = Outer_Syntax.improper_command @{command_spec "print_locales"} "print locales of this theory" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o + Toplevel.keep (Locale.print_locales o Toplevel.theory_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_classes"} @@ -815,44 +820,57 @@ val _ = Outer_Syntax.improper_command @{command_spec "print_locale"} "print locale of this theory" - (opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale)); + (opt_bang -- Parse.position Parse.xname >> (fn (b, name) => + Toplevel.no_timing o Toplevel.unknown_theory o + Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name))); val _ = Outer_Syntax.improper_command @{command_spec "print_interps"} "print interpretations of locale for this theory or proof context" - (Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations)); + (Parse.position Parse.xname >> (fn name => Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name))); val _ = Outer_Syntax.improper_command @{command_spec "print_dependencies"} "print dependencies of locale expression" - (opt_bang -- Parse_Spec.locale_expression true >> - (Toplevel.no_timing oo Isar_Cmd.print_dependencies)); + (opt_bang -- Parse_Spec.locale_expression true >> (fn (clean, expr) => + Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (fn state => + Expression.print_dependencies (Toplevel.context_of state) clean expr))); val _ = Outer_Syntax.improper_command @{command_spec "print_attributes"} "print attributes of this theory" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o + Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_simpset"} "print context of Simplifier" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (fn state => + let val ctxt = Toplevel.context_of state + in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end))); val _ = Outer_Syntax.improper_command @{command_spec "print_rules"} "print intro/elim rules" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (Calculation.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o + Toplevel.keep (Method.print_methods o Toplevel.theory_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of))); val _ = Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies" @@ -872,15 +890,18 @@ val _ = Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context" - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases)); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_statement"}