renamed print_lthms to print_facts, do not insist on proof state;
authorwenzelm
Thu Oct 12 22:57:32 2006 +0200 (2006-10-12 ago)
changeset 2100337492b0062c6
parent 21002 c879f0150db9
child 21004 081674431d68
renamed print_lthms to print_facts, do not insist on proof state;
renamed Toplevel.enter_forward_proof to Toplevel.enter_proof_body;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Oct 12 22:57:29 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Oct 12 22:57:32 2006 +0200
     1.3 @@ -45,6 +45,7 @@
     1.4    val print_context: Toplevel.transition -> Toplevel.transition
     1.5    val print_theory: bool -> Toplevel.transition -> Toplevel.transition
     1.6    val print_syntax: Toplevel.transition -> Toplevel.transition
     1.7 +  val print_facts: Toplevel.transition -> Toplevel.transition
     1.8    val print_theorems: Toplevel.transition -> Toplevel.transition
     1.9    val print_locales: Toplevel.transition -> Toplevel.transition
    1.10    val print_locale: bool * (Locale.expr * Element.context list)
    1.11 @@ -62,7 +63,6 @@
    1.12    val find_theorems: int option * (bool * string FindTheorems.criterion) list
    1.13      -> Toplevel.transition -> Toplevel.transition
    1.14    val print_binds: Toplevel.transition -> Toplevel.transition
    1.15 -  val print_lthms: Toplevel.transition -> Toplevel.transition
    1.16    val print_cases: Toplevel.transition -> Toplevel.transition
    1.17    val print_stmts: string list * (thmref * Attrib.src list) list
    1.18      -> Toplevel.transition -> Toplevel.transition
    1.19 @@ -161,7 +161,7 @@
    1.20    if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
    1.21  
    1.22  val undo = Toplevel.kill o undo_theory o undos_proof 1;
    1.23 -val kill = Toplevel.kill o Toplevel.exit_local_theory o kill_proof;
    1.24 +val kill = Toplevel.kill o kill_proof;
    1.25  
    1.26  val back =
    1.27    Toplevel.actual_proof ProofHistory.back o
    1.28 @@ -225,6 +225,10 @@
    1.29    Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o
    1.30    Toplevel.keep (ProofContext.print_syntax o Proof.context_of o Toplevel.proof_of);
    1.31  
    1.32 +val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
    1.33 +  ProofContext.setmp_verbose
    1.34 +    ProofContext.print_lthms (Context.proof_of (Toplevel.context_of state)));
    1.35 +
    1.36  val print_theorems_proof = Toplevel.keep (fn state =>
    1.37    ProofContext.setmp_verbose
    1.38      ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
    1.39 @@ -289,11 +293,11 @@
    1.40  (* retrieve theorems *)
    1.41  
    1.42  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.43 -  ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_forward_proof state) args));
    1.44 +  ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
    1.45  
    1.46  fun find_theorems (opt_lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.47    let
    1.48 -    val proof_state = Toplevel.enter_forward_proof state;
    1.49 +    val proof_state = Toplevel.enter_proof_body state;
    1.50      val ctxt = Proof.context_of proof_state;
    1.51      val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2);
    1.52    in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end);
    1.53 @@ -305,8 +309,6 @@
    1.54    ProofContext.setmp_verbose
    1.55      ProofContext.print_binds (Proof.context_of (Toplevel.proof_of state)));
    1.56  
    1.57 -val print_lthms = Toplevel.unknown_proof o print_theorems_proof;
    1.58 -
    1.59  val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state =>
    1.60    ProofContext.setmp_verbose
    1.61      ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state)));
    1.62 @@ -365,7 +367,7 @@
    1.63    in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end;
    1.64  
    1.65  fun print_item string_of (modes, arg) = Toplevel.keep (fn state => with_modes modes (fn () =>
    1.66 -  writeln (string_of (Toplevel.enter_forward_proof state) arg)));
    1.67 +  writeln (string_of (Toplevel.enter_proof_body state) arg)));
    1.68  
    1.69  in
    1.70