--- a/src/Pure/PIDE/markup.ML Mon Mar 10 18:06:23 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Mar 10 20:27:08 2014 +0100
@@ -27,6 +27,7 @@
val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
val language_method: T
+ val language_attribute: T
val language_sort: bool -> T
val language_type: bool -> T
val language_term: bool -> T
@@ -277,6 +278,8 @@
val language_method =
language {name = "method", symbols = true, antiquotes = false, delimited = false};
+val language_attribute =
+ language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
val language_type = language' {name = "type", symbols = true, antiquotes = false};
val language_term = language' {name = "term", symbols = true, antiquotes = false};