23354

1 
(* Title: Pure/context_position.ML


2 
ID: $Id$


3 
Author: Makarius


4 


5 
Context positions.


6 
*)


7 


8 
signature CONTEXT_POSITION =


9 
sig


10 
val put: Position.T > Proof.context > Proof.context


11 
val get: Proof.context > Position.T


12 
val str_of: Proof.context > string


13 
end;


14 


15 
structure ContextPosition: CONTEXT_POSITION =


16 
struct


17 


18 
structure Data = ProofDataFun


19 
(


20 
type T = Position.T;


21 
fun init _ = Position.none;


22 
);


23 


24 
val put = Data.put;


25 
val get = Data.get;


26 
val str_of = Position.str_of o get;


27 


28 
end;
