952 fun print_codesetup thy = |
952 fun print_codesetup thy = |
953 let |
953 let |
954 val ctxt = Proof_Context.init_global thy; |
954 val ctxt = Proof_Context.init_global thy; |
955 val exec = the_exec thy; |
955 val exec = the_exec thy; |
956 fun pretty_equations const thms = |
956 fun pretty_equations const thms = |
957 (Pretty.block o Pretty.fbreaks) ( |
957 (Pretty.block o Pretty.fbreaks) |
958 Pretty.str (string_of_const thy const) :: |
958 (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms); |
959 map (Pretty.item o single o Display.pretty_thm ctxt) thms |
|
960 ); |
|
961 fun pretty_function (const, Default (_, eqns_lazy)) = |
959 fun pretty_function (const, Default (_, eqns_lazy)) = |
962 pretty_equations const (map fst (Lazy.force eqns_lazy)) |
960 pretty_equations const (map fst (Lazy.force eqns_lazy)) |
963 | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns) |
961 | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns) |
964 | pretty_function (const, Proj (proj, _)) = Pretty.block |
962 | pretty_function (const, Proj (proj, _)) = Pretty.block |
965 [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj] |
963 [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj] |