maintain mode in context (get/set/restore_mode);
authorwenzelm
Thu Aug 30 15:04:42 2007 +0200 (2007-08-30 ago)
changeset 24484013b98b57b86
parent 24483 0b1a8fd26da9
child 24485 687bbb686ef9
maintain mode in context (get/set/restore_mode);
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Thu Aug 30 15:04:41 2007 +0200
     1.2 +++ b/src/Pure/type.ML	Thu Aug 30 15:04:42 2007 +0200
     1.3 @@ -35,6 +35,9 @@
     1.4    val mode_default: mode
     1.5    val mode_syntax: mode
     1.6    val mode_abbrev: mode
     1.7 +  val get_mode: Proof.context -> mode
     1.8 +  val set_mode: mode -> Proof.context -> Proof.context
     1.9 +  val restore_mode: Proof.context -> Proof.context -> Proof.context
    1.10    val cert_typ_mode: mode -> tsig -> typ -> typ
    1.11    val cert_typ: tsig -> typ -> typ
    1.12    val arity_number: tsig -> string -> int
    1.13 @@ -155,6 +158,16 @@
    1.14  val mode_syntax = Mode {normalize = true, logical = false};
    1.15  val mode_abbrev = Mode {normalize = false, logical = false};
    1.16  
    1.17 +structure Mode = ProofDataFun
    1.18 +(
    1.19 +  type T = mode;
    1.20 +  fun init _ = mode_default;
    1.21 +);
    1.22 +
    1.23 +val get_mode = Mode.get;
    1.24 +fun set_mode mode = Mode.map (K mode);
    1.25 +fun restore_mode ctxt = set_mode (get_mode ctxt);
    1.26 +
    1.27  
    1.28  (* certified types *)
    1.29