changeset 26001 | d0a133941155 |
parent 25982 | caee173104d3 |
child 26051 | 43bcb30a6d97 |
--- a/src/Pure/General/markup.ML Mon Jan 28 22:27:20 2008 +0100 +++ b/src/Pure/General/markup.ML Mon Jan 28 22:27:21 2008 +0100 @@ -20,6 +20,7 @@ val internalK: string val property_internal: property val lineN: string + val columnN: string val fileN: string val positionN: string val position: T val indentN: string @@ -104,6 +105,7 @@ (* position *) val lineN = "line"; +val columnN = "column"; val fileN = "file"; val idN = "id";