# HG changeset patch
# User wenzelm
# Date 1188479082 -7200
# Node ID 013b98b57b86d203cf4f0897f4f9645e5ae882e4
# Parent  0b1a8fd26da98135f8f54efed8f7d33583e39f7d
maintain mode in context (get/set/restore_mode);

diff -r 0b1a8fd26da9 -r 013b98b57b86 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Aug 30 15:04:41 2007 +0200
+++ b/src/Pure/type.ML	Thu Aug 30 15:04:42 2007 +0200
@@ -35,6 +35,9 @@
   val mode_default: mode
   val mode_syntax: mode
   val mode_abbrev: mode
+  val get_mode: Proof.context -> mode
+  val set_mode: mode -> Proof.context -> Proof.context
+  val restore_mode: Proof.context -> Proof.context -> Proof.context
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
   val arity_number: tsig -> string -> int
@@ -155,6 +158,16 @@
 val mode_syntax = Mode {normalize = true, logical = false};
 val mode_abbrev = Mode {normalize = false, logical = false};
 
+structure Mode = ProofDataFun
+(
+  type T = mode;
+  fun init _ = mode_default;
+);
+
+val get_mode = Mode.get;
+fun set_mode mode = Mode.map (K mode);
+fun restore_mode ctxt = set_mode (get_mode ctxt);
+
 
 (* certified types *)