src/Pure/General/position.ML

   val none: T
   val line_file: int -> string -> T
   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
   val str_of: T -> string
   val thread_data: unit -> T

       then Pos (SOME (m, n + 1), props) else pos
   | advance _ pos = pos;
 
 
 (* 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
   | SOME s => Int.fromString s);