export transfer_syntax;
authorwenzelm
Wed Jun 18 18:55:07 2008 +0200 (2008-06-18 ago)
changeset 272596e71abb8c994
parent 27258 656cfac246be
child 27260 17d617c6b026
export transfer_syntax;
added allow_dummies feature (for legacy emulations);
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jun 18 18:55:06 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jun 18 18:55:07 2008 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
     1.5    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
     1.6    val facts_of: Proof.context -> Facts.T
     1.7 +  val transfer_syntax: theory -> Proof.context -> Proof.context
     1.8    val transfer: theory -> Proof.context -> Proof.context
     1.9    val theory: (theory -> theory) -> Proof.context -> Proof.context
    1.10    val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
    1.11 @@ -39,8 +40,6 @@
    1.12    val pretty_thm: Proof.context -> thm -> Pretty.T
    1.13    val pretty_thms: Proof.context -> thm list -> Pretty.T
    1.14    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
    1.15 -  val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
    1.16 -  val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
    1.17    val string_of_thm: Proof.context -> thm -> string
    1.18    val read_typ: Proof.context -> string -> typ
    1.19    val read_typ_syntax: Proof.context -> string -> typ
    1.20 @@ -56,6 +55,7 @@
    1.21    val read_tyname: Proof.context -> string -> typ
    1.22    val read_const_proper: Proof.context -> string -> term
    1.23    val read_const: Proof.context -> string -> term
    1.24 +  val allow_dummies: Proof.context -> Proof.context
    1.25    val decode_term: Proof.context -> term -> term
    1.26    val standard_infer_types: Proof.context -> term list -> term list
    1.27    val read_term_pattern: Proof.context -> string -> term
    1.28 @@ -299,13 +299,6 @@
    1.29    | pretty_fact ctxt (a, ths) =
    1.30        Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
    1.31  
    1.32 -fun pretty_proof ctxt prf =
    1.33 -  pretty_term_abbrev (ctxt |> transfer_syntax (ProofSyntax.proof_syntax prf (theory_of ctxt)))
    1.34 -    (ProofSyntax.term_of_proof prf);
    1.35 -
    1.36 -fun pretty_proof_of ctxt full th =
    1.37 -  pretty_proof ctxt (ProofSyntax.proof_of full th);
    1.38 -
    1.39  val string_of_thm = Pretty.string_of oo pretty_thm;
    1.40  
    1.41  
    1.42 @@ -502,19 +495,24 @@
    1.43  
    1.44  local
    1.45  
    1.46 +structure AllowDummies = ProofDataFun(type T = bool fun init _ = false);
    1.47 +
    1.48 +fun check_dummies ctxt t =
    1.49 +  if AllowDummies.get ctxt then t
    1.50 +  else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
    1.51 +
    1.52  fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
    1.53  
    1.54 -fun reject_dummies t = Term.no_dummy_patterns t
    1.55 -  handle TERM _ => error "Illegal dummy pattern(s) in term";
    1.56 +in
    1.57  
    1.58 -in
    1.59 +val allow_dummies = AllowDummies.put true;
    1.60  
    1.61  fun prepare_patterns ctxt =
    1.62    let val Mode {pattern, ...} = get_mode ctxt in
    1.63      TypeInfer.fixate_params (Variable.names_of ctxt) #>
    1.64      pattern ? Variable.polymorphic ctxt #>
    1.65      (map o Term.map_types) (prepare_patternT ctxt) #>
    1.66 -    (if pattern then prepare_dummies else map reject_dummies)
    1.67 +    (if pattern then prepare_dummies else map (check_dummies ctxt))
    1.68    end;
    1.69  
    1.70  end;