"{-#" $whitechar* (DEPRECATED|deprecated)
{ token ITdeprecated_prag }
"{-#" $whitechar* (SCC|scc) { token ITscc_prag }
+ "{-#" $whitechar* (GENERATED|generated)
+ { token ITgenerated_prag }
"{-#" $whitechar* (CORE|core) { token ITcore_prag }
"{-#" $whitechar* (UNPACK|unpack) { token ITunpack_prag }
| ITdeprecated_prag
| ITline_prag
| ITscc_prag
+ | ITgenerated_prag
| ITcore_prag -- hdaume: core annotations
| ITunpack_prag
| ITclose_prag