diff -r 3069dade3eb4 -r a189707c1d76 src/Pure/context_position.ML --- /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;