# HG changeset patch
# User wenzelm
# Date 1214930321 -7200
# Node ID c0ef698c09041ec7043525609779cf928889688e
# Parent  a54f01b758874135b6f94399a0a17e66b013c919
added get_id/put_id;

diff -r a54f01b75887 -r c0ef698c0904 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Jul 01 09:58:32 2008 +0200
+++ b/src/Pure/General/position.ML	Tue Jul 01 18:38:41 2008 +0200
@@ -16,6 +16,8 @@
   val line: int -> T
   val file: string -> T
   val advance: Symbol.symbol -> T -> T
+  val get_id: T -> string option
+  val put_id: string -> T -> T
   val of_properties: Markup.property list -> T
   val properties_of: T -> Markup.property list
   val default_properties: T -> Markup.property list -> Markup.property list
@@ -57,6 +59,9 @@
 
 (* markup properties *)
 
+fun get_id (Pos (_, props)) = AList.lookup (op =) props Markup.idN;
+fun put_id id (Pos (count, props)) = Pos (count, AList.update (op =) (Markup.idN, id) props);
+
 fun get_int props (name: string) =
   (case AList.lookup (op =) props name of
     NONE => NONE