Context positions.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/context_position.ML	Wed Jun 13 00:01:57 2007 +0200
@@ -0,0 +1,28 @@
+(*  Title:      Pure/context_position.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Context positions.
+*)
+
+signature CONTEXT_POSITION =
+sig
+  val put: Position.T -> Proof.context -> Proof.context
+  val get: Proof.context -> Position.T
+  val str_of: Proof.context -> string
+end;
+
+structure ContextPosition: CONTEXT_POSITION =
+struct
+
+structure Data = ProofDataFun
+(
+  type T = Position.T;
+  fun init _ = Position.none;
+);
+
+val put = Data.put;
+val get = Data.get;
+val str_of = Position.str_of o get;
+
+end;