# HG changeset patch # User wenzelm # Date 1213808108 -7200 # Node ID 17d617c6b026cce2088e2742aa5ec6f27b6d22b8 # Parent 6e71abb8c994214d8898ef672fb9817f59390593 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof; read_term: imitate old behaviour (allow_dummies, mode_schematic); diff -r 6e71abb8c994 -r 17d617c6b026 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Wed Jun 18 18:55:07 2008 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Wed Jun 18 18:55:08 2008 +0200 @@ -19,9 +19,8 @@ val read_proof: theory -> bool -> string -> Proofterm.proof val proof_syntax: Proofterm.proof -> theory -> theory val proof_of: bool -> thm -> Proofterm.proof - val pretty_proof: theory -> Proofterm.proof -> Pretty.T - val pretty_proof_of: bool -> thm -> Pretty.T - val print_proof_of: bool -> thm -> unit + val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T + val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T end; structure ProofSyntax : PROOF_SYNTAX = @@ -98,7 +97,7 @@ val tab = Symtab.fold (fn (key, ps) => fn tab => let val prop = the_default (Bound 0) (AList.lookup (op =) thms' key) - in fst (fold_rev (fn (prop', prf) => fn x as (tab, i) => + in fst (fold_rev (fn (prop', prf) => fn x as (tab, i) => if prop <> prop' then (Symtab.update (key ^ "_" ^ string_of_int i, prf) tab, i+1) else x) ps (tab, 1)) @@ -193,7 +192,7 @@ | term_of _ (PAxm (name, _, SOME Ts)) = mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT)) | term_of _ (PBound i) = Bound i - | term_of Ts (Abst (s, opT, prf)) = + | term_of Ts (Abst (s, opT, prf)) = let val T = the_default dummyT opT in Const ("Abst", (T --> proofT) --> proofT) $ Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) @@ -203,7 +202,7 @@ Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf)) | term_of Ts (prf1 %% prf2) = AppPt $ term_of Ts prf1 $ term_of Ts prf2 - | term_of Ts (prf % opt) = + | term_of Ts (prf % opt) = let val t = the_default (Term.dummy_pattern dummyT) opt in Const ("Appt", [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $ @@ -234,17 +233,22 @@ let val thm_names = filter_out (equal "") (map fst (PureThy.all_thms_of thy)); val axm_names = map fst (Theory.all_axioms_of thy); - val thy' = thy + val ctxt = thy |> add_proof_syntax |> add_proof_atom_consts (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names) - in Sign.simple_read_term thy' end; + |> ProofContext.init + |> ProofContext.allow_dummies + |> ProofContext.set_mode ProofContext.mode_schematic; + in + fn ty => fn s => + (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s + |> TypeInfer.constrain ty |> Syntax.check_term ctxt + end; fun read_proof thy = let val rd = read_term thy proofT - in - (fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s))) - end; + in fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s)) end; fun proof_syntax prf = let @@ -267,12 +271,12 @@ | _ => prf) in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end; -fun pretty_proof thy prf = - Syntax.pretty_term_global (proof_syntax prf thy) (term_of_proof prf); +fun pretty_proof ctxt prf = + ProofContext.pretty_term_abbrev + (ProofContext.transfer_syntax (proof_syntax prf (ProofContext.theory_of ctxt)) ctxt) + (term_of_proof prf); -fun pretty_proof_of full thm = - pretty_proof (Thm.theory_of_thm thm) (proof_of full thm); - -val print_proof_of = Pretty.writeln oo pretty_proof_of; +fun pretty_proof_of ctxt full th = + pretty_proof ctxt (proof_of full th); end;