# HG changeset patch
# User wenzelm
# Date 1199395511 -3600
# Node ID d2a94e6a7d1ed7a10dd20f0eac74cf4212eb50fe
# Parent  c7b1e7b7087bc762ab1f97e9e8f4e897d49dd337
moved id to position properties;

diff -r c7b1e7b7087b -r d2a94e6a7d1e src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Jan 03 22:10:52 2008 +0100
+++ b/src/Pure/General/markup.ML	Thu Jan 03 22:25:11 2008 +0100
@@ -96,7 +96,6 @@
 fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
 
 val nameN = "name";
-val idN = "id";
 
 
 (* kind *)
@@ -111,6 +110,7 @@
 
 val lineN = "line";
 val fileN = "file";
+val idN = "id";
 
 val (positionN, position) = markup_elem "position";