added markup for binding;
tuned;

--- a/src/Pure/General/markup.ML	Tue Mar 03 15:12:52 2009 +0100
+++ b/src/Pure/General/markup.ML	Tue Mar 03 17:42:30 2009 +0100
@@ -12,9 +12,9 @@
   val properties: (string * string) list -> T -> T
   val nameN: string
   val name: string -> T -> T
+  val bindingN: string val binding: string -> T
   val groupN: string
   val theory_nameN: string
-  val idN: string
   val kindN: string
   val internalK: string
   val property_internal: Properties.property
@@ -25,6 +25,7 @@
   val end_columnN: string
   val end_offsetN: string
   val fileN: string
+  val idN: string
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
@@ -107,6 +108,8 @@
 structure Markup: MARKUP =
 struct
 
+(** markup elements **)
+
 (* basic markup *)
 
 type T = string * Properties.T;
@@ -130,6 +133,8 @@
 val nameN = "name";
 fun name a = properties [(nameN, a)];
 
+val (bindingN, binding) = markup_string "binding" nameN;
+
 val groupN = "group";
 val theory_nameN = "theory_name";
 
@@ -278,7 +283,7 @@
 
 
 
-(* print mode operations *)
+(** print mode operations **)
 
 val no_output = ("", "");
 fun default_output (_: T) = no_output;