# HG changeset patch
# User wenzelm
# Date 1217974208 -7200
# Node ID c421ee0d2350df7cb51a8ed39908776fc3e012f3
# Parent  d41abb7bc08a2354783aeaf372d7c1dabba43826
added position_properties';
renamed prop to proposition;
added attribute, method;

diff -r d41abb7bc08a -r c421ee0d2350 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Aug 05 19:29:09 2008 +0200
+++ b/src/Pure/General/markup.ML	Wed Aug 06 00:10:08 2008 +0200
@@ -25,6 +25,7 @@
   val end_lineN: string
   val end_columnN: string
   val fileN: string
+  val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
   val locationN: string val location: T
@@ -51,7 +52,9 @@
   val sortN: string val sort: T
   val typN: string val typ: T
   val termN: string val term: T
-  val propN: string val prop: T
+  val propositionN: string val proposition: T
+  val attributeN: string val attribute: string -> T
+  val methodN: string val method: string -> T
   val keywordN: string val keyword: string -> T
   val commandN: string val command: string -> T
   val keyword_declN: string val keyword_decl: string -> T
@@ -130,7 +133,9 @@
 val fileN = "file";
 val idN = "id";
 
-val position_properties = [lineN, columnN, end_lineN, end_columnN, fileN, idN];
+val position_properties' = [end_lineN, end_columnN, fileN, idN];
+val position_properties = [lineN, columnN] @ position_properties';
+
 val (positionN, position) = markup_elem "position";
 
 val (locationN, location) = markup_elem "location";
@@ -172,7 +177,10 @@
 val (sortN, sort) = markup_elem "sort";
 val (typN, typ) = markup_elem "typ";
 val (termN, term) = markup_elem "term";
-val (propN, prop) = markup_elem "prop";
+val (propositionN, proposition) = markup_elem "proposition";
+
+val (attributeN, attribute) = markup_string "attribute" nameN;
+val (methodN, method) = markup_string "method" nameN;
 
 
 (* outer syntax *)