# HG changeset patch # User wenzelm # Date 1236098550 -3600 # Node ID 14145e81a2fef89fc76df78f40eafc2d962858f1 # Parent 11373ba06bf0c679733e224fd37c748704851b1f added markup for binding; tuned; diff -r 11373ba06bf0 -r 14145e81a2fe src/Pure/General/markup.ML --- 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;