added column property;
authorwenzelm
Mon, 28 Jan 2008 22:27:21 +0100
changeset 26001 d0a133941155
parent 26000 b629b4f2026c
child 26002 469ee728a5d7
added column property;
src/Pure/General/markup.ML
--- 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";