# HG changeset patch # User wenzelm # Date 932054098 -7200 # Node ID ae9dac5af9d13d040e6b6e3f1c17480b77921ce1 # Parent 7e8e9a26ba2cfca80fd0f73a0faf36477a61b823 improved print_thms; diff -r 7e8e9a26ba2c -r ae9dac5af9d1 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Jul 15 17:53:28 1999 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Jul 15 17:54:58 1999 +0200 @@ -35,7 +35,7 @@ val print_methods: Toplevel.transition -> Toplevel.transition val print_binds: Toplevel.transition -> Toplevel.transition val print_lthms: Toplevel.transition -> Toplevel.transition - val print_thms: xstring * Args.src list -> Toplevel.transition -> Toplevel.transition + val print_thms: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition val print_prop: string -> Toplevel.transition -> Toplevel.transition val print_term: string -> Toplevel.transition -> Toplevel.transition val print_type: string -> Toplevel.transition -> Toplevel.transition @@ -125,26 +125,13 @@ val print_lthms = Toplevel.keep (ProofContext.print_thms o Proof.context_of o Toplevel.proof_of); -(* print theorems *) - -fun global_attribs thy ths srcs = - #2 (Thm.applys_attributes ((Theory.copy thy, ths), map (Attrib.global_attribute thy) srcs)); - -fun local_attribs st ths srcs = - #2 (Thm.applys_attributes ((Proof.context_of st, ths), - map (Attrib.local_attribute (Proof.theory_of st)) srcs)); +(* print theorems / types / terms / props *) -fun print_thms (name, srcs) = Toplevel.keep (fn state => - let - val ths = map (Thm.transfer (Toplevel.theory_of state)) - (Toplevel.node_case PureThy.get_thms (ProofContext.get_thms o Proof.context_of) - state name); - val ths' = Toplevel.node_case global_attribs local_attribs state ths srcs; - in Display.print_thms ths' end); +fun print_thms args = Toplevel.keep (fn state => + let val st = Toplevel.node_case Proof.init_state Proof.enter_forward state + in Display.print_thms (IsarThy.get_thmss args st) end); -(* print types, terms and props *) - fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None); fun read_term T thy s = diff -r 7e8e9a26ba2c -r ae9dac5af9d1 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Jul 15 17:53:28 1999 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Jul 15 17:54:58 1999 +0200 @@ -463,7 +463,7 @@ (Scan.succeed IsarCmd.print_lthms); val print_thmsP = - OuterSyntax.improper_command "thm" "print theorems" K.diag (P.xthm >> IsarCmd.print_thms); + OuterSyntax.improper_command "thm" "print theorems" K.diag (P.xthms1 >> IsarCmd.print_thms); val print_propP = OuterSyntax.improper_command "prop" "read and print proposition" K.diag diff -r 7e8e9a26ba2c -r ae9dac5af9d1 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Thu Jul 15 17:53:28 1999 +0200 +++ b/src/Pure/Isar/isar_thy.ML Thu Jul 15 17:54:58 1999 +0200 @@ -123,6 +123,7 @@ val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition + val get_thmss: (string * Args.src list) list -> Proof.state -> thm list val also: ((string * Args.src list) list * Comment.interest) option * Comment.text -> Toplevel.transition -> Toplevel.transition val also_i: (thm list * Comment.interest) option * Comment.text @@ -224,20 +225,20 @@ gen_have_thmss (ProofContext.get_thms o Proof.context_of) (Attrib.local_attribute o Proof.theory_of) x; -fun have_thmss_i f ((name, more_atts), th_atts) = +fun gen_have_thmss_i f ((name, more_atts), th_atts) = f name more_atts (map (apfst single) th_atts); fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]); fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss ((None, []), th_srcs); -fun apply_theorems_i th_srcs = have_thmss_i PureThy.have_thmss ((None, []), th_srcs); +fun apply_theorems_i th_srcs = gen_have_thmss_i PureThy.have_thmss ((None, []), th_srcs); val have_theorems = #1 oo (global_have_thmss (PureThy.have_thmss o Some) o Comment.ignore); -val have_theorems_i = #1 oo (have_thmss_i (PureThy.have_thmss o Some) o Comment.ignore); +val have_theorems_i = #1 oo (gen_have_thmss_i (PureThy.have_thmss o Some) o Comment.ignore); val have_lemmas = #1 oo (global_have_thmss (have_lemss o Some) o Comment.ignore); -val have_lemmas_i = #1 oo (have_thmss_i (have_lemss o Some) o Comment.ignore); +val have_lemmas_i = #1 oo (gen_have_thmss_i (have_lemss o Some) o Comment.ignore); val have_facts = ProofHistory.apply o local_have_thmss (Proof.have_thmss []) o Comment.ignore; -val have_facts_i = ProofHistory.apply o have_thmss_i (Proof.have_thmss []) o Comment.ignore; +val have_facts_i = ProofHistory.apply o gen_have_thmss_i (Proof.have_thmss []) o Comment.ignore; (* forward chaining *) @@ -248,9 +249,9 @@ Proof.have_thmss (Proof.the_facts state) name atts ths_atts state; val from_facts = gen_from_facts (local_have_thmss (Proof.have_thmss [])) o Comment.ignore; -val from_facts_i = gen_from_facts (have_thmss_i (Proof.have_thmss [])) o Comment.ignore; +val from_facts_i = gen_from_facts (gen_have_thmss_i (Proof.have_thmss [])) o Comment.ignore; val with_facts = gen_from_facts (local_have_thmss add_thmss) o Comment.ignore; -val with_facts_i = gen_from_facts (have_thmss_i add_thmss) o Comment.ignore; +val with_facts_i = gen_from_facts (gen_have_thmss_i add_thmss) o Comment.ignore; fun chain comment_ignore = ProofHistory.apply Proof.chain; fun export_chain comment_ignore = ProofHistory.applys Proof.export_chain; @@ -383,14 +384,14 @@ fun proof''' f = Toplevel.proof' (f o cond_print_calc); -fun get_thmss srcs = Proof.the_facts o local_have_thmss (Proof.have_thmss []) (("", []), srcs); -fun get_thmss_i thms _ = thms; - fun gen_calc get f (args, _) prt state = f (apsome (fn (srcs, _) => get srcs state) args) prt state; in +fun get_thmss srcs = Proof.the_facts o local_have_thmss (Proof.have_thmss []) (("", []), srcs); +fun get_thmss_i thms _ = thms; + fun also x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.also x); fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x); fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);