# HG changeset patch
# User wenzelm
# Date 1191162035 -7200
# Node ID ec3a04e6f1a96955f53f1551fe355e076af18a22
# Parent  2b838dfeca1e4da6db1dd2f7c9c013a619338e40
added properties_of;

diff -r 2b838dfeca1e -r ec3a04e6f1a9 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Sun Sep 30 16:20:34 2007 +0200
+++ b/src/Pure/context_position.ML	Sun Sep 30 16:20:35 2007 +0200
@@ -10,6 +10,7 @@
   val put: Position.T -> Proof.context -> Proof.context
   val get: Proof.context -> Position.T
   val str_of: Proof.context -> string
+  val properties_of: Proof.context -> Markup.property list
 end;
 
 structure ContextPosition: CONTEXT_POSITION =
@@ -24,5 +25,6 @@
 val put = Data.put;
 val get = Data.get;
 val str_of = Position.str_of o get;
+val properties_of = Position.properties_of o get;
 
 end;