# HG changeset patch
# User wenzelm
# Date 1139534577 -3600
# Node ID 2427684c201cc2909e29c78a8e5cd14fbea9db9a
# Parent  197851f71eef9b53cbcc704ab7a21635b9ec8af8
* ML/Pure: generic Args/Attrib syntax everywhere;

diff -r 197851f71eef -r 2427684c201c NEWS
--- a/NEWS	Fri Feb 10 02:22:56 2006 +0100
+++ b/NEWS	Fri Feb 10 02:22:57 2006 +0100
@@ -374,11 +374,15 @@
 vs. local (Proof.context) attributes have been discontinued, while
 minimizing code duplication.  Thm.rule_attribute and
 Thm.declaration_attribute build canonical attributes; see also
-structure Context for further operations on Context.generic.
-
-INCOMPATIBILITY, need to adapt attribute type declarations and
-definitions.  Hint: make proper use of GenericDataFun and generic
-Args/Attrib syntax instead of working around legacy code.
+structure Context for further operations on Context.generic, notably
+GenericDataFun.  INCOMPATIBILITY, need to adapt attribute type
+declarations and definitions.
+
+* Pure/Isar: Args/Attrib parsers operate on Context.generic --
+global/local versions on theory vs. Proof.context have been
+discontinued; Attrib.syntax and Method.syntax have been adapted
+accordingly.  INCOMPATIBILITY, need to adapt parser expressions for
+attributes, methods, etc.
 
 * Pure: several functions of signature "... -> theory -> theory * ..."
 have been reoriented to "... -> theory -> ... * theory" in order to