unknown_theory/proof/context;
authorwenzelm
Thu Aug 03 18:44:24 2000 +0200 (2000-08-03 ago)
changeset 95138531c18d9181
parent 9512 c30f6d0f81d2
child 9514 8cd9cfc22dd7
unknown_theory/proof/context;
src/Provers/classical.ML
src/Provers/simplifier.ML
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Provers/classical.ML	Thu Aug 03 18:43:35 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu Aug 03 18:44:24 2000 +0200
     1.3 @@ -1193,7 +1193,7 @@
     1.4  val print_clasetP =
     1.5    OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
     1.6      OuterSyntax.Keyword.diag
     1.7 -    (Scan.succeed (Toplevel.no_timing o (Toplevel.keep
     1.8 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
     1.9        (Toplevel.node_case print_claset (print_local_claset o Proof.context_of)))));
    1.10  
    1.11  val _ = OuterSyntax.add_parsers [print_clasetP];
     2.1 --- a/src/Provers/simplifier.ML	Thu Aug 03 18:43:35 2000 +0200
     2.2 +++ b/src/Provers/simplifier.ML	Thu Aug 03 18:44:24 2000 +0200
     2.3 @@ -548,7 +548,7 @@
     2.4  val print_simpsetP =
     2.5    OuterSyntax.improper_command "print_simpset" "print context of Simplifier"
     2.6      OuterSyntax.Keyword.diag
     2.7 -    (Scan.succeed (Toplevel.no_timing o (Toplevel.keep
     2.8 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
     2.9        (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of)))));
    2.10  
    2.11  val _ = OuterSyntax.add_parsers [print_simpsetP];
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 03 18:43:35 2000 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 03 18:44:24 2000 +0200
     3.3 @@ -164,30 +164,51 @@
     3.4  fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
     3.5  
     3.6  
     3.7 -(* print theory *)
     3.8 +(* print parts of theory and proof context *)
     3.9  
    3.10  val print_context = Toplevel.keep Toplevel.print_state_context;
    3.11 -val print_theory = Toplevel.keep (PureThy.print_theory o Toplevel.theory_of);
    3.12 -val print_syntax = Toplevel.keep (Display.print_syntax o Toplevel.theory_of);
    3.13 -val print_theorems = Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of);
    3.14 -val print_attributes = Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
    3.15 -val print_trans_rules = Toplevel.keep (Toplevel.node_case Calculation.print_global_rules
    3.16 -  (Calculation.print_local_rules o Proof.context_of));
    3.17 -val print_methods = Toplevel.keep (Method.print_methods o Toplevel.theory_of);
    3.18 +
    3.19 +val print_theory = Toplevel.unknown_theory o
    3.20 +  Toplevel.keep (PureThy.print_theory o Toplevel.theory_of);
    3.21 +
    3.22 +val print_syntax = Toplevel.unknown_theory o
    3.23 +  Toplevel.keep (Display.print_syntax o Toplevel.theory_of);
    3.24 +
    3.25 +val print_theorems = Toplevel.unknown_theory o
    3.26 +  Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of);
    3.27 +
    3.28 +val print_attributes = Toplevel.unknown_theory o
    3.29 +  Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
    3.30 +
    3.31 +val print_trans_rules = Toplevel.unknown_context o
    3.32 +  Toplevel.keep (Toplevel.node_case Calculation.print_global_rules
    3.33 +    (Calculation.print_local_rules o Proof.context_of));
    3.34 +
    3.35 +val print_methods = Toplevel.unknown_theory o
    3.36 +  Toplevel.keep (Method.print_methods o Toplevel.theory_of);
    3.37 +
    3.38  val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
    3.39  
    3.40 -fun print_thms_containing cs = Toplevel.keep (fn state =>
    3.41 -  ThmDatabase.print_thms_containing (Toplevel.theory_of state) cs);
    3.42 +fun print_thms_containing cs = Toplevel.unknown_theory o
    3.43 +  Toplevel.keep (fn state => ThmDatabase.print_thms_containing (Toplevel.theory_of state) cs);
    3.44  
    3.45 -fun thm_deps args = Toplevel.keep (fn state =>
    3.46 +fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    3.47    ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
    3.48  
    3.49  
    3.50  (* print proof context contents *)
    3.51  
    3.52 -val print_binds = Toplevel.keep (ProofContext.print_binds o Proof.context_of o Toplevel.proof_of);
    3.53 -val print_lthms = Toplevel.keep (ProofContext.print_thms o Proof.context_of o Toplevel.proof_of);
    3.54 -val print_cases = Toplevel.keep (ProofContext.print_cases o Proof.context_of o Toplevel.proof_of);
    3.55 +val print_binds = Toplevel.unknown_proof o Toplevel.keep (fn state =>
    3.56 +  ProofContext.setmp_verbose
    3.57 +    ProofContext.print_binds (Proof.context_of (Toplevel.proof_of state)));
    3.58 +
    3.59 +val print_lthms = Toplevel.unknown_proof o Toplevel.keep (fn state =>
    3.60 +  ProofContext.setmp_verbose
    3.61 +    ProofContext.print_thms (Proof.context_of (Toplevel.proof_of state)));
    3.62 +
    3.63 +val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state =>
    3.64 +  ProofContext.setmp_verbose
    3.65 +    ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state)));
    3.66  
    3.67  
    3.68  (* print theorems / types / terms / props *)