pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
authorwenzelm
Sun Sep 05 19:47:40 2010 +0200 (2010-09-05 ago)
changeset 3913370d3915c92f0
parent 39132 ba17ca3acdd3
child 39134 917b4b6ba3d2
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
src/HOL/Mutabelle/mutabelle_extra.ML
src/Pure/Isar/class.ML
src/Pure/Isar/local_defs.ML
src/Pure/axclass.ML
src/Pure/more_thm.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Sep 04 22:36:42 2010 +0200
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Sep 05 19:47:40 2010 +0200
     1.3 @@ -315,7 +315,6 @@
     1.4  (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
     1.5  fun mutate_theorem create_entry thy mtds thm =
     1.6    let
     1.7 -    val pp = Syntax.pp_global thy
     1.8      val exec = is_executable_thm thy thm
     1.9      val _ = priority (if exec then "EXEC" else "NOEXEC")
    1.10      val mutants =
    1.11 @@ -343,7 +342,7 @@
    1.12            |> map Mutabelle.freeze |> map freezeT
    1.13  (*          |> filter (not o is_forbidden_mutant) *)
    1.14            |> List.mapPartial (try (Sign.cert_term thy))
    1.15 -    val _ = map (fn t => priority ("MUTANT: " ^ Pretty.string_of (Pretty.term pp t))) mutants
    1.16 +    val _ = map (fn t => priority ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
    1.17    in
    1.18      create_entry thy thm exec mutants mtds
    1.19    end
     2.1 --- a/src/Pure/Isar/class.ML	Sat Sep 04 22:36:42 2010 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Sun Sep 05 19:47:40 2010 +0200
     2.3 @@ -525,9 +525,8 @@
     2.4      val params = map_product get_param tycos class_params |> map_filter I;
     2.5      val primary_constraints = map (apsnd
     2.6        (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
     2.7 -    val pp = Syntax.pp_global thy;
     2.8      val algebra = Sign.classes_of thy
     2.9 -      |> fold (fn tyco => Sorts.add_arities pp
    2.10 +      |> fold (fn tyco => Sorts.add_arities (Syntax.pp_global thy)
    2.11              (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
    2.12      val consts = Sign.consts_of thy;
    2.13      val improve_constraints = AList.lookup (op =)
     3.1 --- a/src/Pure/Isar/local_defs.ML	Sat Sep 04 22:36:42 2010 +0200
     3.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Sep 05 19:47:40 2010 +0200
     3.3 @@ -47,7 +47,7 @@
     3.4      fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^
     3.5        quote (Syntax.string_of_term ctxt eq));
     3.6      val ((lhs, _), eq') = eq
     3.7 -      |> Sign.no_vars (Syntax.pp ctxt)
     3.8 +      |> Sign.no_vars ctxt
     3.9        |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
    3.10        handle TERM (msg, _) => err msg | ERROR msg => err msg;
    3.11    in (Term.dest_Free (Term.head_of lhs), eq') end;
     4.1 --- a/src/Pure/axclass.ML	Sat Sep 04 22:36:42 2010 +0200
     4.2 +++ b/src/Pure/axclass.ML	Sun Sep 05 19:47:40 2010 +0200
     4.3 @@ -507,8 +507,7 @@
     4.4  
     4.5  fun define_class (bclass, raw_super) raw_params raw_specs thy =
     4.6    let
     4.7 -    val ctxt = ProofContext.init_global thy;
     4.8 -    val pp = Syntax.pp ctxt;
     4.9 +    val ctxt = Syntax.init_pretty_global thy;
    4.10  
    4.11  
    4.12      (* class *)
    4.13 @@ -520,8 +519,8 @@
    4.14      fun check_constraint (a, S) =
    4.15        if Sign.subsort thy (super, S) then ()
    4.16        else error ("Sort constraint of type variable " ^
    4.17 -        setmp_CRITICAL show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
    4.18 -        " needs to be weaker than " ^ Pretty.string_of_sort pp super);
    4.19 +        setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) (TFree (a, S)) ^
    4.20 +        " needs to be weaker than " ^ Syntax.string_of_sort ctxt super);
    4.21  
    4.22  
    4.23      (* params *)
    4.24 @@ -543,7 +542,7 @@
    4.25        (case Term.add_tfrees t [] of
    4.26          [(a, S)] => check_constraint (a, S)
    4.27        | [] => ()
    4.28 -      | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t);
    4.29 +      | _ => error ("Multiple type variables in class axiom:\n" ^ Syntax.string_of_term ctxt t);
    4.30        t
    4.31        |> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
    4.32        |> Logic.close_form);
    4.33 @@ -590,7 +589,7 @@
    4.34        |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2
    4.35        |> Sign.restore_naming facts_thy
    4.36        |> map_axclasses (Symtab.update (class, axclass))
    4.37 -      |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
    4.38 +      |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
    4.39  
    4.40    in (class, result_thy) end;
    4.41  
     5.1 --- a/src/Pure/more_thm.ML	Sat Sep 04 22:36:42 2010 +0200
     5.2 +++ b/src/Pure/more_thm.ML	Sun Sep 05 19:47:40 2010 +0200
     5.3 @@ -348,7 +348,7 @@
     5.4    let
     5.5      val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
     5.6  
     5.7 -    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
     5.8 +    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
     5.9      val (strip, recover, prop') = stripped_sorts thy prop;
    5.10      val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
    5.11      val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
    5.12 @@ -365,7 +365,7 @@
    5.13  
    5.14  fun add_def unchecked overloaded (b, prop) thy =
    5.15    let
    5.16 -    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
    5.17 +    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
    5.18      val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
    5.19      val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
    5.20  
     6.1 --- a/src/Pure/sign.ML	Sat Sep 04 22:36:42 2010 +0200
     6.2 +++ b/src/Pure/sign.ML	Sun Sep 05 19:47:40 2010 +0200
     6.3 @@ -67,8 +67,8 @@
     6.4    val certify_term: theory -> term -> term * typ * int
     6.5    val cert_term: theory -> term -> term
     6.6    val cert_prop: theory -> term -> term
     6.7 -  val no_frees: Pretty.pp -> term -> term
     6.8 -  val no_vars: Pretty.pp -> term -> term
     6.9 +  val no_frees: Proof.context -> term -> term
    6.10 +  val no_vars: Proof.context -> term -> term
    6.11    val add_types: (binding * int * mixfix) list -> theory -> theory
    6.12    val add_nonterminals: binding list -> theory -> theory
    6.13    val add_type_abbrev: binding * string list * typ -> theory -> theory
    6.14 @@ -320,12 +320,13 @@
    6.15  
    6.16  (* specifications *)
    6.17  
    6.18 -fun no_variables kind add addT mk mkT pp tm =
    6.19 +fun no_variables kind add addT mk mkT ctxt tm =
    6.20    (case (add tm [], addT tm []) of
    6.21      ([], []) => tm
    6.22    | (frees, tfrees) => error (Pretty.string_of (Pretty.block
    6.23        (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") :: Pretty.brk 1 ::
    6.24 -       Pretty.commas (map (Pretty.term pp o mk) frees @ map (Pretty.typ pp o mkT) tfrees)))));
    6.25 +       Pretty.commas
    6.26 +        (map (Syntax.pretty_term ctxt o mk) frees @ map (Syntax.pretty_typ ctxt o mkT) tfrees)))));
    6.27  
    6.28  val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
    6.29  val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
    6.30 @@ -434,12 +435,12 @@
    6.31  
    6.32  fun add_abbrev mode (b, raw_t) thy =
    6.33    let
    6.34 -    val pp = Syntax.pp_global thy;
    6.35 -    val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
    6.36 +    val ctxt = Syntax.init_pretty_global thy;
    6.37 +    val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy;
    6.38      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    6.39        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
    6.40      val (res, consts') = consts_of thy
    6.41 -      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode (b, t);
    6.42 +      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of thy) (naming_of thy) mode (b, t);
    6.43    in (res, thy |> map_consts (K consts')) end;
    6.44  
    6.45  fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
     7.1 --- a/src/Pure/theory.ML	Sat Sep 04 22:36:42 2010 +0200
     7.2 +++ b/src/Pure/theory.ML	Sun Sep 05 19:47:40 2010 +0200
     7.3 @@ -167,7 +167,7 @@
     7.4        error ("Illegal sort constraints in primitive specification: " ^
     7.5          commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
     7.6    in
     7.7 -    (b, Sign.no_vars (Syntax.pp_global thy) t)
     7.8 +    (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
     7.9    end handle ERROR msg =>
    7.10      cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
    7.11  
    7.12 @@ -182,10 +182,10 @@
    7.13  
    7.14  fun dependencies thy unchecked def description lhs rhs =
    7.15    let
    7.16 -    val pp = Syntax.pp_global thy;
    7.17 +    val ctxt = Syntax.init_pretty_global thy;
    7.18      val consts = Sign.consts_of thy;
    7.19      fun prep const =
    7.20 -      let val Const (c, T) = Sign.no_vars pp (Const const)
    7.21 +      let val Const (c, T) = Sign.no_vars ctxt (Const const)
    7.22        in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
    7.23  
    7.24      val lhs_vars = Term.add_tfreesT (#2 lhs) [];
    7.25 @@ -194,9 +194,9 @@
    7.26      val _ =
    7.27        if null rhs_extras then ()
    7.28        else error ("Specification depends on extra type variables: " ^
    7.29 -        commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
    7.30 +        commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
    7.31          "\nThe error(s) above occurred in " ^ quote description);
    7.32 -  in Defs.define pp unchecked def description (prep lhs) (map prep rhs) end;
    7.33 +  in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
    7.34  
    7.35  fun add_deps a raw_lhs raw_rhs thy =
    7.36    let
     8.1 --- a/src/Tools/Code/code_preproc.ML	Sat Sep 04 22:36:42 2010 +0200
     8.2 +++ b/src/Tools/Code/code_preproc.ML	Sun Sep 05 19:47:40 2010 +0200
     8.3 @@ -429,10 +429,9 @@
     8.4  
     8.5  fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
     8.6    let
     8.7 -    val pp = Syntax.pp_global thy;
     8.8 +    val ctxt = Syntax.init_pretty_global thy;
     8.9      val ct = cterm_of proto_ct;
    8.10 -    val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
    8.11 -      (Thm.term_of ct);
    8.12 +    val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
    8.13      val thm = preprocess_conv thy ct;
    8.14      val ct' = Thm.rhs_of thm;
    8.15      val (vs', t') = dest_cterm ct';