489 fun pretty_term_typeof ctxt (style, t) = |
489 fun pretty_term_typeof ctxt (style, t) = |
490 Syntax.pretty_typ ctxt (Term.fastype_of (style t)); |
490 Syntax.pretty_typ ctxt (Term.fastype_of (style t)); |
491 |
491 |
492 fun pretty_const ctxt c = |
492 fun pretty_const ctxt c = |
493 let |
493 let |
494 val t = Const (c, Consts.type_scheme (ProofContext.consts_of ctxt) c) |
494 val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c) |
495 handle TYPE (msg, _, _) => error msg; |
495 handle TYPE (msg, _, _) => error msg; |
496 val ([t'], _) = Variable.import_terms true [t] ctxt; |
496 val ([t'], _) = Variable.import_terms true [t] ctxt; |
497 in pretty_term ctxt t' end; |
497 in pretty_term ctxt t' end; |
498 |
498 |
499 fun pretty_abbrev ctxt s = |
499 fun pretty_abbrev ctxt s = |
500 let |
500 let |
501 val t = Syntax.parse_term ctxt s |> singleton (ProofContext.standard_infer_types ctxt); |
501 val t = Syntax.parse_term ctxt s |> singleton (Proof_Context.standard_infer_types ctxt); |
502 fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t); |
502 fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t); |
503 val (head, args) = Term.strip_comb t; |
503 val (head, args) = Term.strip_comb t; |
504 val (c, T) = Term.dest_Const head handle TERM _ => err (); |
504 val (c, T) = Term.dest_Const head handle TERM _ => err (); |
505 val (U, u) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c |
505 val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c |
506 handle TYPE _ => err (); |
506 handle TYPE _ => err (); |
507 val t' = Term.betapplys (Envir.expand_atom T (U, u), args); |
507 val t' = Term.betapplys (Envir.expand_atom T (U, u), args); |
508 val eq = Logic.mk_equals (t, t'); |
508 val eq = Logic.mk_equals (t, t'); |
509 val ctxt' = Variable.auto_fixes eq ctxt; |
509 val ctxt' = Variable.auto_fixes eq ctxt; |
510 in ProofContext.pretty_term_abbrev ctxt' eq end; |
510 in Proof_Context.pretty_term_abbrev ctxt' eq end; |
511 |
511 |
512 fun pretty_class ctxt = |
512 fun pretty_class ctxt = |
513 Pretty.str o ProofContext.extern_class ctxt o ProofContext.read_class ctxt; |
513 Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt; |
514 |
514 |
515 fun pretty_type ctxt s = |
515 fun pretty_type ctxt s = |
516 let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s |
516 let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s |
517 in Pretty.str (ProofContext.extern_type ctxt name) end; |
517 in Pretty.str (Proof_Context.extern_type ctxt name) end; |
518 |
518 |
519 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full; |
519 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full; |
520 |
520 |
521 fun pretty_theory ctxt name = |
521 fun pretty_theory ctxt name = |
522 (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name); |
522 (Theory.requires (Proof_Context.theory_of ctxt) name "presentation"; Pretty.str name); |
523 |
523 |
524 |
524 |
525 (* default output *) |
525 (* default output *) |
526 |
526 |
527 val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src; |
527 val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src; |