# HG changeset patch
# User wenzelm
# Date 1201555641 -3600
# Node ID d0a133941155659f095a48dc2813fd737f5e3dd4
# Parent  b629b4f2026ca09bd8ff076bb4ec20be55a65e31
added column property;

diff -r b629b4f2026c -r d0a133941155 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";