tuned -- less indirection;
authorwenzelm
Sat Jan 05 16:16:22 2013 +0100 (2013-01-05 ago)
changeset 50737f310d1735d93
parent 50736 07dfdf72ab75
child 50738 d5725e56cd04
tuned -- less indirection;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Jan 05 11:24:09 2013 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Jan 05 16:16:22 2013 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.5    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.6    val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
     1.7 -  val add_axioms: (Attrib.binding * string) list -> theory -> theory
     1.8    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
     1.9    val declaration: {syntax: bool, pervasive: bool} ->
    1.10      Symbol_Pos.text * Position.T -> local_theory -> local_theory
    1.11 @@ -42,32 +41,13 @@
    1.12    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
    1.13    val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
    1.14    val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
    1.15 -  val print_context: Toplevel.transition -> Toplevel.transition
    1.16 -  val print_theory: bool -> Toplevel.transition -> Toplevel.transition
    1.17 -  val print_syntax: Toplevel.transition -> Toplevel.transition
    1.18 -  val print_abbrevs: Toplevel.transition -> Toplevel.transition
    1.19 -  val print_facts: Toplevel.transition -> Toplevel.transition
    1.20 -  val print_configs: Toplevel.transition -> Toplevel.transition
    1.21    val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
    1.22 -  val print_locales: Toplevel.transition -> Toplevel.transition
    1.23 -  val print_locale: bool * (xstring * Position.T) -> Toplevel.transition -> Toplevel.transition
    1.24 -  val print_registrations: xstring * Position.T -> Toplevel.transition -> Toplevel.transition
    1.25 -  val print_dependencies: bool * Expression.expression -> Toplevel.transition
    1.26 -    -> Toplevel.transition
    1.27 -  val print_attributes: Toplevel.transition -> Toplevel.transition
    1.28 -  val print_simpset: Toplevel.transition -> Toplevel.transition
    1.29 -  val print_rules: Toplevel.transition -> Toplevel.transition
    1.30 -  val print_trans_rules: Toplevel.transition -> Toplevel.transition
    1.31 -  val print_methods: Toplevel.transition -> Toplevel.transition
    1.32 -  val print_antiquotations: Toplevel.transition -> Toplevel.transition
    1.33    val thy_deps: Toplevel.transition -> Toplevel.transition
    1.34    val locale_deps: Toplevel.transition -> Toplevel.transition
    1.35    val class_deps: Toplevel.transition -> Toplevel.transition
    1.36    val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
    1.37    val unused_thms: (string list * string list option) option ->
    1.38      Toplevel.transition -> Toplevel.transition
    1.39 -  val print_binds: Toplevel.transition -> Toplevel.transition
    1.40 -  val print_cases: Toplevel.transition -> Toplevel.transition
    1.41    val print_stmts: string list * (Facts.ref * Attrib.src list) list
    1.42      -> Toplevel.transition -> Toplevel.transition
    1.43    val print_thms: string list * (Facts.ref * Attrib.src list) list
    1.44 @@ -187,9 +167,7 @@
    1.45    in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end;
    1.46  
    1.47  
    1.48 -(* old-style axioms *)
    1.49 -
    1.50 -val add_axioms = fold (snd oo Specification.axiom_cmd);
    1.51 +(* old-style defs *)
    1.52  
    1.53  fun add_defs ((unchecked, overloaded), args) thy =
    1.54    thy |>
    1.55 @@ -328,24 +306,7 @@
    1.56    in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
    1.57  
    1.58  
    1.59 -(* print parts of theory and proof context *)
    1.60 -
    1.61 -val print_context = Toplevel.keep Toplevel.print_state_context;
    1.62 -
    1.63 -fun print_theory verbose = Toplevel.unknown_theory o
    1.64 -  Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of);
    1.65 -
    1.66 -val print_syntax = Toplevel.unknown_context o
    1.67 -  Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of);
    1.68 -
    1.69 -val print_abbrevs = Toplevel.unknown_context o
    1.70 -  Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of);
    1.71 -
    1.72 -val print_facts = Toplevel.unknown_context o
    1.73 -  Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of);
    1.74 -
    1.75 -val print_configs = Toplevel.unknown_context o
    1.76 -  Toplevel.keep (Attrib.print_configs o Toplevel.context_of);
    1.77 +(* print theorems *)
    1.78  
    1.79  val print_theorems_proof =
    1.80    Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of);
    1.81 @@ -359,39 +320,8 @@
    1.82  fun print_theorems verbose =
    1.83    Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof;
    1.84  
    1.85 -val print_locales = Toplevel.unknown_theory o
    1.86 -  Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
    1.87  
    1.88 -fun print_locale (verbose, name) = Toplevel.unknown_theory o
    1.89 -  Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) verbose name);
    1.90 -
    1.91 -fun print_registrations name = Toplevel.unknown_context o
    1.92 -  Toplevel.keep (fn state =>
    1.93 -    Locale.print_registrations (Toplevel.context_of state) name);
    1.94 -
    1.95 -fun print_dependencies (clean, expression) = Toplevel.unknown_context o
    1.96 -  Toplevel.keep (fn state =>
    1.97 -    Expression.print_dependencies (Toplevel.context_of state) clean expression);
    1.98 -
    1.99 -val print_attributes = Toplevel.unknown_theory o
   1.100 -  Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
   1.101 -
   1.102 -val print_simpset = Toplevel.unknown_context o
   1.103 -  Toplevel.keep (fn state =>
   1.104 -    let val ctxt = Toplevel.context_of state
   1.105 -    in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end);
   1.106 -
   1.107 -val print_rules = Toplevel.unknown_context o
   1.108 -  Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of);
   1.109 -
   1.110 -val print_trans_rules = Toplevel.unknown_context o
   1.111 -  Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
   1.112 -
   1.113 -val print_methods = Toplevel.unknown_theory o
   1.114 -  Toplevel.keep (Method.print_methods o Toplevel.theory_of);
   1.115 -
   1.116 -val print_antiquotations =
   1.117 -  Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of);
   1.118 +(* display dependencies *)
   1.119  
   1.120  val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   1.121    let
   1.122 @@ -454,15 +384,6 @@
   1.123    end);
   1.124  
   1.125  
   1.126 -(* print proof context contents *)
   1.127 -
   1.128 -val print_binds = Toplevel.unknown_context o
   1.129 -  Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of);
   1.130 -
   1.131 -val print_cases = Toplevel.unknown_context o
   1.132 -  Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of);
   1.133 -
   1.134 -
   1.135  (* print theorems, terms, types etc. *)
   1.136  
   1.137  local
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jan 05 11:24:09 2013 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jan 05 16:16:22 2013 +0100
     2.3 @@ -174,7 +174,7 @@
     2.4      (Scan.repeat1 Parse_Spec.spec >>
     2.5        (fn spec => Toplevel.theory (fn thy =>
     2.6          (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
     2.7 -          Isar_Cmd.add_axioms spec thy))));
     2.8 +          fold (snd oo Specification.axiom_cmd) spec thy))));
     2.9  
    2.10  val opt_unchecked_overloaded =
    2.11    Scan.optional (@{keyword "("} |-- Parse.!!!
    2.12 @@ -775,26 +775,30 @@
    2.13  
    2.14  val _ =
    2.15    Outer_Syntax.improper_command @{command_spec "print_configs"} "print configuration options"
    2.16 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));
    2.17 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    2.18 +      Toplevel.keep (Attrib.print_configs o Toplevel.context_of)));
    2.19  
    2.20  val _ =
    2.21 -  Outer_Syntax.improper_command @{command_spec "print_context"} "print theory context name"
    2.22 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));
    2.23 +  Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
    2.24 +    (Scan.succeed (Toplevel.no_timing o Toplevel.keep Toplevel.print_state_context));
    2.25  
    2.26  val _ =
    2.27    Outer_Syntax.improper_command @{command_spec "print_theory"}
    2.28      "print logical theory contents (verbose!)"
    2.29 -    (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
    2.30 +    (opt_bang >> (fn b => Toplevel.no_timing o Toplevel.unknown_theory o
    2.31 +      Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
    2.32  
    2.33  val _ =
    2.34    Outer_Syntax.improper_command @{command_spec "print_syntax"}
    2.35      "print inner syntax of context (verbose!)"
    2.36 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
    2.37 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    2.38 +      Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
    2.39  
    2.40  val _ =
    2.41    Outer_Syntax.improper_command @{command_spec "print_abbrevs"}
    2.42      "print constant abbreviation of context"
    2.43 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
    2.44 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    2.45 +      Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
    2.46  
    2.47  val _ =
    2.48    Outer_Syntax.improper_command @{command_spec "print_theorems"}
    2.49 @@ -804,7 +808,8 @@
    2.50  val _ =
    2.51    Outer_Syntax.improper_command @{command_spec "print_locales"}
    2.52      "print locales of this theory"
    2.53 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));
    2.54 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    2.55 +      Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
    2.56  
    2.57  val _ =
    2.58    Outer_Syntax.improper_command @{command_spec "print_classes"}
    2.59 @@ -815,44 +820,57 @@
    2.60  val _ =
    2.61    Outer_Syntax.improper_command @{command_spec "print_locale"}
    2.62      "print locale of this theory"
    2.63 -    (opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
    2.64 +    (opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
    2.65 +      Toplevel.no_timing o Toplevel.unknown_theory o
    2.66 +      Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
    2.67  
    2.68  val _ =
    2.69    Outer_Syntax.improper_command @{command_spec "print_interps"}
    2.70      "print interpretations of locale for this theory or proof context"
    2.71 -    (Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
    2.72 +    (Parse.position Parse.xname >> (fn name => Toplevel.no_timing o Toplevel.unknown_context o
    2.73 +      Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
    2.74  
    2.75  val _ =
    2.76    Outer_Syntax.improper_command @{command_spec "print_dependencies"}
    2.77      "print dependencies of locale expression"
    2.78 -    (opt_bang -- Parse_Spec.locale_expression true >>
    2.79 -      (Toplevel.no_timing oo Isar_Cmd.print_dependencies));
    2.80 +    (opt_bang -- Parse_Spec.locale_expression true >> (fn (clean, expr) =>
    2.81 +      Toplevel.no_timing o Toplevel.unknown_context o
    2.82 +        Toplevel.keep (fn state =>
    2.83 +          Expression.print_dependencies (Toplevel.context_of state) clean expr)));
    2.84  
    2.85  val _ =
    2.86    Outer_Syntax.improper_command @{command_spec "print_attributes"}
    2.87      "print attributes of this theory"
    2.88 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
    2.89 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    2.90 +      Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of)));
    2.91  
    2.92  val _ =
    2.93    Outer_Syntax.improper_command @{command_spec "print_simpset"}
    2.94      "print context of Simplifier"
    2.95 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));
    2.96 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    2.97 +      Toplevel.keep (fn state =>
    2.98 +        let val ctxt = Toplevel.context_of state
    2.99 +        in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end)));
   2.100  
   2.101  val _ =
   2.102    Outer_Syntax.improper_command @{command_spec "print_rules"} "print intro/elim rules"
   2.103 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));
   2.104 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   2.105 +      Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
   2.106  
   2.107  val _ =
   2.108    Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
   2.109 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));
   2.110 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   2.111 +      Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
   2.112  
   2.113  val _ =
   2.114    Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
   2.115 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
   2.116 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   2.117 +      Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
   2.118  
   2.119  val _ =
   2.120    Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
   2.121 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
   2.122 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   2.123 +      Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
   2.124  
   2.125  val _ =
   2.126    Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
   2.127 @@ -872,15 +890,18 @@
   2.128  
   2.129  val _ =
   2.130    Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
   2.131 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));
   2.132 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   2.133 +      Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of)));
   2.134  
   2.135  val _ =
   2.136    Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
   2.137 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));
   2.138 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   2.139 +      Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of)));
   2.140  
   2.141  val _ =
   2.142    Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
   2.143 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));
   2.144 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   2.145 +      Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of)));
   2.146  
   2.147  val _ =
   2.148    Outer_Syntax.improper_command @{command_spec "print_statement"}