src/Pure/Isar/isar_cmd.ML
changeset 56868 b5fb264d53ba
parent 56334 6b3739fee456
child 57605 8e0a7eaffe47
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon May 05 16:30:19 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon May 05 17:14:46 2014 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
     1.5    val diag_state: Proof.context -> Toplevel.state
     1.6    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
     1.7 -  val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
     1.8 +  val pretty_theorems: bool -> Toplevel.state -> Pretty.T
     1.9    val thy_deps: Toplevel.transition -> Toplevel.transition
    1.10    val locale_deps: Toplevel.transition -> Toplevel.transition
    1.11    val class_deps: Toplevel.transition -> Toplevel.transition
    1.12 @@ -258,20 +258,19 @@
    1.13      (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
    1.14  
    1.15  
    1.16 -(* print theorems *)
    1.17 -
    1.18 -fun print_theorems_proof verbose =
    1.19 -  Toplevel.keep (fn st =>
    1.20 -    Proof_Context.print_local_facts (Proof.context_of (Toplevel.proof_of st)) verbose);
    1.21 +(* theorems of theory or proof context *)
    1.22  
    1.23 -fun print_theorems_theory verbose = Toplevel.keep (fn state =>
    1.24 -  Toplevel.theory_of state |>
    1.25 -  (case Toplevel.previous_context_of state of
    1.26 -    SOME prev => Proof_Display.print_theorems_diff verbose (Proof_Context.theory_of prev)
    1.27 -  | NONE => Proof_Display.print_theorems verbose));
    1.28 -
    1.29 -fun print_theorems verbose =
    1.30 -  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof verbose;
    1.31 +fun pretty_theorems verbose st =
    1.32 +  if Toplevel.is_proof st then
    1.33 +    Pretty.chunks (Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose)
    1.34 +  else
    1.35 +    let
    1.36 +      val thy = Toplevel.theory_of st;
    1.37 +      val prev_thys =
    1.38 +        (case Toplevel.previous_context_of st of
    1.39 +          SOME prev => [Proof_Context.theory_of prev]
    1.40 +        | NONE => Theory.parents_of thy);
    1.41 +    in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
    1.42  
    1.43  
    1.44  (* display dependencies *)