src/Pure/context_position.ML

+(*  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;