src/Pure/context_position.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24791 fb1830099265
permissions -rw-r--r--
Name.uu, Name.aT;
     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 -> Context.generic -> Context.generic
    11   val put_ctxt: Position.T -> Proof.context -> Proof.context
    12   val get: Proof.context -> Position.T
    13   val str_of: Proof.context -> string
    14   val properties_of: Proof.context -> Markup.property list
    15 end;
    16 
    17 structure ContextPosition: CONTEXT_POSITION =
    18 struct
    19 
    20 structure Data = GenericDataFun
    21 (
    22   type T = Position.T;
    23   val empty = Position.none;
    24   fun extend _ = empty;
    25   fun merge _ _ = empty;
    26 );
    27 
    28 val put = Data.put;
    29 val put_ctxt = Context.proof_map o put;
    30 
    31 val get = Data.get o Context.Proof;
    32 val str_of = Position.str_of o get;
    33 val properties_of = Position.properties_of o get;
    34 
    35 end;