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

24791

10 
val put: Position.T > Context.generic > Context.generic


11 
val put_ctxt: Position.T > Proof.context > Proof.context

23354

12 
val get: Proof.context > Position.T


13 
val str_of: Proof.context > string

24773

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

23354

15 
end;


16 


17 
structure ContextPosition: CONTEXT_POSITION =


18 
struct


19 

24791

20 
structure Data = GenericDataFun

23354

21 
(


22 
type T = Position.T;

24791

23 
val empty = Position.none;


24 
fun extend _ = empty;


25 
fun merge _ _ = empty;

23354

26 
);


27 


28 
val put = Data.put;

24791

29 
val put_ctxt = Context.proof_map o put;


30 


31 
val get = Data.get o Context.Proof;

23354

32 
val str_of = Position.str_of o get;

24773

33 
val properties_of = Position.properties_of o get;

23354

34 


35 
end;
