author | wenzelm |
Thu, 03 Jan 2008 22:25:11 +0100 | |
changeset 25816 | d2a94e6a7d1e |
parent 25815 | c7b1e7b7087b |
child 25817 | d8e0190917a5 |
--- 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";