src/Pure/context_position.ML
changeset 24791 fb1830099265
parent 24773 ec3a04e6f1a9
equal deleted inserted replaced
24790:3be1580de4cc 24791:fb1830099265
     5 Context positions.
     5 Context positions.
     6 *)
     6 *)
     7 
     7 
     8 signature CONTEXT_POSITION =
     8 signature CONTEXT_POSITION =
     9 sig
     9 sig
    10   val put: Position.T -> Proof.context -> Proof.context
    10   val put: Position.T -> Context.generic -> Context.generic
       
    11   val put_ctxt: Position.T -> Proof.context -> Proof.context
    11   val get: Proof.context -> Position.T
    12   val get: Proof.context -> Position.T
    12   val str_of: Proof.context -> string
    13   val str_of: Proof.context -> string
    13   val properties_of: Proof.context -> Markup.property list
    14   val properties_of: Proof.context -> Markup.property list
    14 end;
    15 end;
    15 
    16 
    16 structure ContextPosition: CONTEXT_POSITION =
    17 structure ContextPosition: CONTEXT_POSITION =
    17 struct
    18 struct
    18 
    19 
    19 structure Data = ProofDataFun
    20 structure Data = GenericDataFun
    20 (
    21 (
    21   type T = Position.T;
    22   type T = Position.T;
    22   fun init _ = Position.none;
    23   val empty = Position.none;
       
    24   fun extend _ = empty;
       
    25   fun merge _ _ = empty;
    23 );
    26 );
    24 
    27 
    25 val put = Data.put;
    28 val put = Data.put;
    26 val get = Data.get;
    29 val put_ctxt = Context.proof_map o put;
       
    30 
       
    31 val get = Data.get o Context.Proof;
    27 val str_of = Position.str_of o get;
    32 val str_of = Position.str_of o get;
    28 val properties_of = Position.properties_of o get;
    33 val properties_of = Position.properties_of o get;
    29 
    34 
    30 end;
    35 end;