src/Pure/General/markup.ML

   val none: T
   val is_none: T -> bool
   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
   val lineN: string
   val columnN: string
   val offsetN: string
   val end_lineN: string
   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
   val locationN: string val location: T
   val indentN: string

 end;
 
 structure Markup: MARKUP =
 struct
 
+(** markup elements **)
+
 (* basic markup *)
 
 type T = string * Properties.T;
 
 val none = ("", []);

 
 (* name *)
 
 val nameN = "name";
 fun name a = properties [(nameN, a)];
+
+val (bindingN, binding) = markup_string "binding" nameN;
 
 val groupN = "group";
 val theory_nameN = "theory_name";
 
 

 
 val (promptN, prompt) = markup_elem "prompt";
 
 
 
-(* print mode operations *)
+(** print mode operations **)
 
 val no_output = ("", "");
 fun default_output (_: T) = no_output;
 
 local