| changeset 41484 | 51310e1ccd6f |
| parent 41483 | 4a8431c73cf2 |
| child 42012 | 2c3fe3cbebae |
--- a/src/Pure/General/markup.ML Sun Jan 09 16:03:56 2011 +0100 +++ b/src/Pure/General/markup.ML Sun Jan 09 20:30:47 2011 +0100 @@ -189,8 +189,8 @@ val fileN = "file"; val idN = "id"; -val position_properties' = [end_offsetN, fileN, idN]; -val position_properties = [lineN, columnN, offsetN] @ position_properties'; +val position_properties' = [fileN, idN]; +val position_properties = [lineN, columnN, offsetN, end_offsetN] @ position_properties'; val (positionN, position) = markup_elem "position";