# HG changeset patch
# User wenzelm
# Date 1230907472 -3600
# Node ID 3a0b38b7fbb471d4487dad8cde98aaa56bb37640
# Parent  2c764235e041cb27d88f985de238bc81c7f228fd
added id;
tuned;

diff -r 2c764235e041 -r 3a0b38b7fbb4 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri Jan 02 11:31:40 2009 +0100
+++ b/src/Pure/General/position.ML	Fri Jan 02 15:44:32 2009 +0100
@@ -1,8 +1,7 @@
 (*  Title:      Pure/General/position.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Source positions: counting Isabelle symbols -- starting from 1.
+Source positions: counting Isabelle symbols, starting from 1.
 *)
 
 signature POSITION =
@@ -19,6 +18,7 @@
   val file: string -> T
   val line: int -> T
   val line_file: int -> string -> T
+  val id: string -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
   val of_properties: Properties.T -> T
@@ -86,6 +86,7 @@
 val none = Pos ((0, 0, 0), []);
 val start = Pos ((1, 1, 1), []);
 
+
 fun file_name "" = []
   | file_name name = [(Markup.fileN, name)];
 
@@ -95,11 +96,14 @@
 fun line i = line_file i "";
 
 
-(* markup properties *)
+fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]);
 
 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
 fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
 
+
+(* markup properties *)
+
 fun of_properties props =
   let
     fun get name =