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

24773

13 
val properties_of: Proof.context > Markup.property list

23354

14 
end;


15 


16 
structure ContextPosition: CONTEXT_POSITION =


17 
struct


18 


19 
structure Data = ProofDataFun


20 
(


21 
type T = Position.T;


22 
fun init _ = Position.none;


23 
);


24 


25 
val put = Data.put;


26 
val get = Data.get;


27 
val str_of = Position.str_of o get;

24773

28 
val properties_of = Position.properties_of o get;

23354

29 


30 
end;
