# HG changeset patch # User wenzelm # Date 1192111530 -7200 # Node ID 5298ee9c3fe5ce9f403b825ec9df0abac95bc8f1 # Parent 39d1dd215d7326d4f951b2e2910770e55d121084 moved ProofContext.pp to Syntax.pp; diff -r 39d1dd215d73 -r 5298ee9c3fe5 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Thu Oct 11 16:05:26 2007 +0200 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Thu Oct 11 16:05:30 2007 +0200 @@ -228,7 +228,7 @@ fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) fun pr_goals ctxt st = - Display.pretty_goals_aux (ProofContext.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st + Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st |> Pretty.chunks |> Pretty.string_of diff -r 39d1dd215d73 -r 5298ee9c3fe5 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Thu Oct 11 16:05:26 2007 +0200 +++ b/src/Pure/Isar/local_defs.ML Thu Oct 11 16:05:30 2007 +0200 @@ -40,7 +40,7 @@ fun cert_def ctxt eq = let - val pp = ProofContext.pp ctxt; + val pp = Syntax.pp ctxt; val display_term = quote o Pretty.string_of_term pp; fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq); val ((lhs, _), eq') = eq diff -r 39d1dd215d73 -r 5298ee9c3fe5 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Oct 11 16:05:26 2007 +0200 +++ b/src/Pure/Isar/proof.ML Thu Oct 11 16:05:30 2007 +0200 @@ -317,7 +317,7 @@ val show_main_goal = ref false; val verbose = ProofContext.verbose; -val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp; +val pretty_goals_local = Display.pretty_goals_aux o Syntax.pp; fun pretty_facts _ _ NONE = [] | pretty_facts s ctxt (SOME ths) = diff -r 39d1dd215d73 -r 5298ee9c3fe5 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Oct 11 16:05:26 2007 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Oct 11 16:05:30 2007 +0200 @@ -34,7 +34,6 @@ val transfer: theory -> Proof.context -> Proof.context val theory: (theory -> theory) -> Proof.context -> Proof.context val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context - val pp: Proof.context -> Pretty.pp val pretty_term_abbrev: Proof.context -> term -> Pretty.T val pretty_thm_legacy: thm -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T @@ -293,23 +292,15 @@ (** pretty printing **) -(*pp operations -- deferred evaluation*) -fun pp ctxt = Pretty.pp - (fn x => Syntax.pretty_term ctxt x, - fn x => Syntax.pretty_typ ctxt x, - fn x => Syntax.pretty_sort ctxt x, - fn x => Syntax.pretty_classrel ctxt x, - fn x => Syntax.pretty_arity ctxt x); - fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); fun pretty_thm_legacy th = let val thy = Thm.theory_of_thm th - in Display.pretty_thm_aux (pp (init thy)) true false [] th end; + in Display.pretty_thm_aux (Syntax.pp (init thy)) true false [] th end; fun pretty_thm ctxt th = let val asms = map Thm.term_of (Assumption.assms_of ctxt) - in Display.pretty_thm_aux (pp ctxt) false true asms th end; + in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end; fun pretty_thms ctxt [th] = pretty_thm ctxt th | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths)); @@ -411,7 +402,7 @@ fun certify_consts ctxt = let val Mode {abbrev, ...} = get_mode ctxt - in Consts.certify (pp ctxt) (tsig_of ctxt) (not abbrev) (consts_of ctxt) end; + in Consts.certify (Syntax.pp ctxt) (tsig_of ctxt) (not abbrev) (consts_of ctxt) end; fun reject_schematic (Var (xi, _)) = error ("Unbound schematic variable: " ^ Term.string_of_vname xi) @@ -534,7 +525,7 @@ val sorts = append_env (Variable.def_sort ctxt) more_sorts; val used = fold Name.declare more_used (Variable.names_of ctxt); in - (read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) + (read (Syntax.pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) (legacy_intern_skolem ctxt internal types) s handle TERM (msg, _) => error msg) |> app (expand_abbrevs ctxt) @@ -561,7 +552,7 @@ fun gen_cert prop ctxt t = t |> expand_abbrevs ctxt - |> (fn t' => #1 (Sign.certify' prop (pp ctxt) false (consts_of ctxt) (theory_of ctxt) t') + |> (fn t' => #1 (Sign.certify' prop (Syntax.pp ctxt) false (consts_of ctxt) (theory_of ctxt) t') handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg); @@ -577,7 +568,7 @@ fun standard_infer_types ctxt ts = let val Mode {pattern, ...} = get_mode ctxt in - TypeInfer.infer_types (pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt) + TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt) (try (Consts.the_constraint (consts_of ctxt))) (Variable.def_type ctxt pattern) (Variable.names_of ctxt) (Variable.maxidx_of ctxt) NONE (map (rpair dummyT) ts) |> #1 |> map #1 @@ -662,8 +653,9 @@ TypeInfer.constrain T; fun check t = Exn.Result (infer t) handle ERROR msg => Exn.Exn (ERROR msg); val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt; - val read = Syntax.standard_parse_term (pp ctxt) check get_sort map_const map_free map_type - map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) ((#1 (TypeInfer.paramify_dummies T 0))); + val read = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort + map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) + ((#1 (TypeInfer.paramify_dummies T 0))); in read str end; @@ -1042,7 +1034,7 @@ handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; val ((lhs, rhs), consts') = consts_of ctxt - |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (c, t); + |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (c, t); in ctxt |> map_consts (apsnd (K consts'))