author | wenzelm |
Mon, 28 Jan 2008 22:27:21 +0100 | |
changeset 26001 | d0a133941155 |
parent 26000 | b629b4f2026c |
child 26002 | 469ee728a5d7 |
--- 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";