src/Pure/Isar/isar_cmd.ML
changeset 5913 c543568ccaca
parent 5895 457b42674b57
child 5991 832ec852fc4e
equal deleted inserted replaced
5912:3f95adea10c0 5913:c543568ccaca
    24   val print_attributes: Toplevel.transition -> Toplevel.transition
    24   val print_attributes: Toplevel.transition -> Toplevel.transition
    25   val print_methods: Toplevel.transition -> Toplevel.transition
    25   val print_methods: Toplevel.transition -> Toplevel.transition
    26   val print_binds: Toplevel.transition -> Toplevel.transition
    26   val print_binds: Toplevel.transition -> Toplevel.transition
    27   val print_lthms: Toplevel.transition -> Toplevel.transition
    27   val print_lthms: Toplevel.transition -> Toplevel.transition
    28   val print_thms: xstring * Args.src list -> Toplevel.transition -> Toplevel.transition
    28   val print_thms: xstring * Args.src list -> Toplevel.transition -> Toplevel.transition
    29   val print_thm: xstring * Args.src list -> Toplevel.transition -> Toplevel.transition
       
    30   val print_prop: string -> Toplevel.transition -> Toplevel.transition
    29   val print_prop: string -> Toplevel.transition -> Toplevel.transition
    31   val print_term: string -> Toplevel.transition -> Toplevel.transition
    30   val print_term: string -> Toplevel.transition -> Toplevel.transition
    32   val print_type: string -> Toplevel.transition -> Toplevel.transition
    31   val print_type: string -> Toplevel.transition -> Toplevel.transition
    33 end;
    32 end;
    34 
    33 
    36 struct
    35 struct
    37 
    36 
    38 
    37 
    39 (* variations on exit *)
    38 (* variations on exit *)
    40 
    39 
    41 val break = Toplevel.imperative (fn () => raise Toplevel.BREAK);
    40 val break = Toplevel.keep (fn state => raise Toplevel.BREAK state);
    42 
    41 
    43 val exit = Toplevel.keep (fn state =>
    42 val exit = Toplevel.keep (fn state =>
    44   (Context.set_context (try Toplevel.theory_of state);
    43   (Context.set_context (try Toplevel.theory_of state);
    45     writeln "Leaving the Isar loop.  Invoke 'main_loop();' to restart.";
    44     writeln "Leaving the Isar loop.  Invoke 'main_loop();' to restart.";
    46     raise Toplevel.TERMINATE));
    45     raise Toplevel.TERMINATE));
   101 
   100 
   102 fun local_attribs st ths srcs =
   101 fun local_attribs st ths srcs =
   103   #2 (Attribute.applys ((Proof.context_of st, ths),
   102   #2 (Attribute.applys ((Proof.context_of st, ths),
   104     map (Attrib.local_attribute (Proof.theory_of st)) srcs));
   103     map (Attrib.local_attribute (Proof.theory_of st)) srcs));
   105 
   104 
   106 fun gen_print_thms global_get local_get (name, srcs) = Toplevel.keep (fn state =>
   105 fun print_thms (name, srcs) = Toplevel.keep (fn state =>
   107   let
   106   let
   108     val prt_tthm = Attribute.pretty_tthm;
       
   109     fun prt_tthms [th] = prt_tthm th
       
   110       | prt_tthms ths = Pretty.block (Pretty.fbreaks (map prt_tthm ths));
       
   111 
       
   112     val ths = map (apfst (Thm.transfer (Toplevel.theory_of state)))
   107     val ths = map (apfst (Thm.transfer (Toplevel.theory_of state)))
   113       (Toplevel.node_cases global_get (local_get o Proof.context_of)
   108       (Toplevel.node_cases PureThy.get_tthms (ProofContext.get_tthms o Proof.context_of)
   114         state name);
   109         state name);
   115     val ths' = Toplevel.node_cases global_attribs local_attribs state ths srcs;
   110     val ths' = Toplevel.node_cases global_attribs local_attribs state ths srcs;
   116   in Pretty.writeln (prt_tthms ths') end);
   111   in Attribute.print_tthms ths' end);
   117 
       
   118 val print_thms = gen_print_thms PureThy.get_tthms ProofContext.get_tthms;
       
   119 val print_thm =
       
   120   gen_print_thms (Library.single oo PureThy.get_tthm) (Library.single oo ProofContext.get_tthm);
       
   121 
   112 
   122 
   113 
   123 (* print types, terms and props *)
   114 (* print types, terms and props *)
   124 
   115 
   125 fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None);
   116 fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None);