# HG changeset patch
# User wenzelm
# Date 1191244493 -7200
# Node ID fb1830099265ef14619ec4d9be447e518a057ff8
# Parent  3be1580de4cc5d09919281248b27f5baeee00b99
turned into generic context data;

diff -r 3be1580de4cc -r fb1830099265 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Mon Oct 01 15:14:51 2007 +0200
+++ b/src/Pure/context_position.ML	Mon Oct 01 15:14:53 2007 +0200
@@ -7,7 +7,8 @@
 
 signature CONTEXT_POSITION =
 sig
-  val put: Position.T -> Proof.context -> Proof.context
+  val put: Position.T -> Context.generic -> Context.generic
+  val put_ctxt: Position.T -> Proof.context -> Proof.context
   val get: Proof.context -> Position.T
   val str_of: Proof.context -> string
   val properties_of: Proof.context -> Markup.property list
@@ -16,14 +17,18 @@
 structure ContextPosition: CONTEXT_POSITION =
 struct
 
-structure Data = ProofDataFun
+structure Data = GenericDataFun
 (
   type T = Position.T;
-  fun init _ = Position.none;
+  val empty = Position.none;
+  fun extend _ = empty;
+  fun merge _ _ = empty;
 );
 
 val put = Data.put;
-val get = Data.get;
+val put_ctxt = Context.proof_map o put;
+
+val get = Data.get o Context.Proof;
 val str_of = Position.str_of o get;
 val properties_of = Position.properties_of o get;