src/Pure/Isar/attrib.ML
2014-03-08 wenzelm 2014-03-08 keep current context visibility for PIDE markup and completion (in contrast to 8e3e004f1c31): Attrib.check_src of 9dc5ce83202c should intern/report attributes once, which happens for local_theory in the (visible) auxiliary context;
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-03-05 wenzelm 2014-03-05 clarified init_assignable: make double-sure that initial values are reset; more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-25 wenzelm 2014-02-25 more positions; tuned messages;
2014-01-25 wenzelm 2014-01-25 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-08-23 wenzelm 2013-08-23 tuned signature;
2013-08-16 wenzelm 2013-08-16 more markup via Name_Space.check; tuned signature;
2013-07-19 wenzelm 2013-07-19 turned pattern unify flag into configuration option (global only);
2013-07-17 wenzelm 2013-07-17 more official Thm.eq_thm_strict, without demanding ML equality type;
2013-06-30 wenzelm 2013-06-30 backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
2013-06-27 wenzelm 2013-06-27 manage option "proofs" within theory context -- with minor overhead for primitive inferences;
2013-05-17 wenzelm 2013-05-17 renamed 'print_configs' to 'print_options';
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-05-16 wenzelm 2013-05-16 system options as context-sensitive configuration options within the attribute name space;
2013-05-16 wenzelm 2013-05-16 tuned signature;
2013-02-11 webertj 2013-02-11 Typo in description of abs_def.
2013-01-08 wenzelm 2013-01-08 allow negative argument in "consumes" source format; more documentation/NEWS;
2012-11-30 wenzelm 2012-11-30 print formal entities with markup;
2012-09-29 wenzelm 2012-09-29 turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-07-06 wenzelm 2012-07-06 discontinued obsolete attribute "COMP";
2012-04-27 wenzelm 2012-04-27 prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
2012-04-27 wenzelm 2012-04-27 clarified signature;
2012-04-01 wenzelm 2012-04-01 added Attrib.global_notes/local_notes/generic_notes convenience;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-03-13 wenzelm 2012-03-13 suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
2012-03-13 wenzelm 2012-03-13 improved attribute "abs_def" to handle object-equality as well;
2012-03-03 wenzelm 2012-03-03 canonical argument order for attribute application;
2012-02-17 wenzelm 2012-02-17 simplified configuration options for syntax ambiguity;
2012-02-16 wenzelm 2012-02-16 simplified configuration options for syntax ambiguity;
2012-01-05 wenzelm 2012-01-05 discontinued Syntax.positions -- atomic parse trees are always annotated;
2011-11-23 wenzelm 2011-11-23 tuned;
2011-11-21 wenzelm 2011-11-21 drop vacuous decls;
2011-11-19 wenzelm 2011-11-19 refined partial evaluation of attributes: avoid duplication of facts for plain declarations; tuned;
2011-11-19 wenzelm 2011-11-19 do not store vacuous theorem specifications -- relevant for frugal local theory content; tuned;
2011-11-17 wenzelm 2011-11-17 partial evaluation in invisible context;
2011-11-16 wenzelm 2011-11-16 retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
2011-11-16 wenzelm 2011-11-16 clarified Attrib.partial_evaluation;
2011-11-14 wenzelm 2011-11-14 some support for partial evaluation of attributed facts;
2011-11-14 wenzelm 2011-11-14 eliminated dead code;
2011-11-07 wenzelm 2011-11-07 tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-08-06 kleing 2011-08-06 make syntax ambiguity warnings a config option
2011-08-08 wenzelm 2011-08-08 made SML/NJ happy;
2011-08-06 nipkow 2011-08-06 extended user-level attribute case_names with names for case hypotheses
2011-06-10 wenzelm 2011-06-10 tuned name (cf. blast_stats);
2011-05-15 wenzelm 2011-05-15 optional description for 'attribute_setup' and 'method_setup';
2011-05-14 wenzelm 2011-05-14 discontinued global config options within attribute name space;
2011-05-03 wenzelm 2011-05-03 more conventional naming scheme: names_long, names_short, names_unique;
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-17 wenzelm 2011-04-17 markup attributes/methods via name space; eliminated obsolete markup;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 discontinued special status of structure Printer;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-07 wenzelm 2011-04-07 tuned signature;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;