break: exhibit state;
authorwenzelm
Tue Nov 17 14:12:13 1998 +0100 (1998-11-17 ago)
changeset 5913c543568ccaca
parent 5912 3f95adea10c0
child 5914 2c069b0a98ee
break: exhibit state;
removed print_thm;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 17 14:11:38 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 17 14:12:13 1998 +0100
     1.3 @@ -26,7 +26,6 @@
     1.4    val print_binds: Toplevel.transition -> Toplevel.transition
     1.5    val print_lthms: Toplevel.transition -> Toplevel.transition
     1.6    val print_thms: xstring * Args.src list -> Toplevel.transition -> Toplevel.transition
     1.7 -  val print_thm: xstring * Args.src list -> Toplevel.transition -> Toplevel.transition
     1.8    val print_prop: string -> Toplevel.transition -> Toplevel.transition
     1.9    val print_term: string -> Toplevel.transition -> Toplevel.transition
    1.10    val print_type: string -> Toplevel.transition -> Toplevel.transition
    1.11 @@ -38,7 +37,7 @@
    1.12  
    1.13  (* variations on exit *)
    1.14  
    1.15 -val break = Toplevel.imperative (fn () => raise Toplevel.BREAK);
    1.16 +val break = Toplevel.keep (fn state => raise Toplevel.BREAK state);
    1.17  
    1.18  val exit = Toplevel.keep (fn state =>
    1.19    (Context.set_context (try Toplevel.theory_of state);
    1.20 @@ -103,21 +102,13 @@
    1.21    #2 (Attribute.applys ((Proof.context_of st, ths),
    1.22      map (Attrib.local_attribute (Proof.theory_of st)) srcs));
    1.23  
    1.24 -fun gen_print_thms global_get local_get (name, srcs) = Toplevel.keep (fn state =>
    1.25 +fun print_thms (name, srcs) = Toplevel.keep (fn state =>
    1.26    let
    1.27 -    val prt_tthm = Attribute.pretty_tthm;
    1.28 -    fun prt_tthms [th] = prt_tthm th
    1.29 -      | prt_tthms ths = Pretty.block (Pretty.fbreaks (map prt_tthm ths));
    1.30 -
    1.31      val ths = map (apfst (Thm.transfer (Toplevel.theory_of state)))
    1.32 -      (Toplevel.node_cases global_get (local_get o Proof.context_of)
    1.33 +      (Toplevel.node_cases PureThy.get_tthms (ProofContext.get_tthms o Proof.context_of)
    1.34          state name);
    1.35      val ths' = Toplevel.node_cases global_attribs local_attribs state ths srcs;
    1.36 -  in Pretty.writeln (prt_tthms ths') end);
    1.37 -
    1.38 -val print_thms = gen_print_thms PureThy.get_tthms ProofContext.get_tthms;
    1.39 -val print_thm =
    1.40 -  gen_print_thms (Library.single oo PureThy.get_tthm) (Library.single oo ProofContext.get_tthm);
    1.41 +  in Attribute.print_tthms ths' end);
    1.42  
    1.43  
    1.44  (* print types, terms and props *)