added properties_of;
authorwenzelm
Sun Sep 30 16:20:35 2007 +0200 (2007-09-30)
changeset 24773ec3a04e6f1a9
parent 24772 2b838dfeca1e
child 24774 bc31c318e673
added properties_of;
src/Pure/context_position.ML
     1.1 --- a/src/Pure/context_position.ML	Sun Sep 30 16:20:34 2007 +0200
     1.2 +++ b/src/Pure/context_position.ML	Sun Sep 30 16:20:35 2007 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    val put: Position.T -> Proof.context -> Proof.context
     1.5    val get: Proof.context -> Position.T
     1.6    val str_of: Proof.context -> string
     1.7 +  val properties_of: Proof.context -> Markup.property list
     1.8  end;
     1.9  
    1.10  structure ContextPosition: CONTEXT_POSITION =
    1.11 @@ -24,5 +25,6 @@
    1.12  val put = Data.put;
    1.13  val get = Data.get;
    1.14  val str_of = Position.str_of o get;
    1.15 +val properties_of = Position.properties_of o get;
    1.16  
    1.17  end;