src/Pure/Isar/args.ML
2014-03-06 wenzelm 2014-03-06 more uniform check_const/read_const;
2014-03-06 wenzelm 2014-03-06 tuned signature -- more uniform check_type_name/read_type_name; proper reports for read_type_name (lost in 710bc66f432c);
2014-03-05 wenzelm 2014-03-05 suppress short abbreviations more uniformly, for outer and quasi-outer syntax; 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 tuned message -- more markup;
2014-02-24 wenzelm 2014-02-24 tuned signature;
2014-02-23 wenzelm 2014-02-23 tuned message;
2014-01-27 wenzelm 2014-01-27 tuned signature;
2014-01-22 wenzelm 2014-01-22 tuned signature;
2014-01-19 wenzelm 2014-01-19 cartouche within nested args (attributes, methods, etc.);
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-08-23 wenzelm 2013-08-23 tuned signature;
2013-08-20 wenzelm 2013-08-20 more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;
2013-08-20 wenzelm 2013-08-20 proper exhaustive match (cf. e9beabf045ab);
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2011-10-28 wenzelm 2011-10-28 tuned signature -- refined terminology;
2011-08-21 wenzelm 2011-08-21 tuned Parse.group: delayed failure message;
2011-04-23 wenzelm 2011-04-23 proper binding/report of defined simprocs; tuned signature;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-10-30 wenzelm 2010-10-30 support for real valued configuration options;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-04-29 wenzelm 2010-04-29 ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;
2010-03-13 wenzelm 2010-03-13 removed unused Args.maxidx_values and Element.generalize_facts;
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2010-02-27 wenzelm 2010-02-27 clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2010-02-25 wenzelm 2010-02-25 clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-02-06 wenzelm 2010-02-06 fixed spelling;
2009-11-10 wenzelm 2009-11-10 bang_facts: legacy feature;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-13 wenzelm 2009-03-13 simplified goal_spec: default to first goal;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-12 wenzelm 2009-03-12 Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-03 wenzelm 2009-03-03 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-09-02 wenzelm 2008-09-02 added binding; thm_name/opt_thm_name: Name.binding;
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-08-10 wenzelm 2008-08-10 pass token source to typ/term etc.;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token; moved datatype value/slot and basic operations to outer_lex.ML; removed unused terminator; removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML); removed obsolete thm_sel (cf. attrib.ML); one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);
2008-08-04 wenzelm 2008-08-04 abstract type Scan.stopper;
2008-06-28 wenzelm 2008-06-28 tuned nested args parser; export generic_args1;
2008-06-28 wenzelm 2008-06-28 added thm_name, opt_thm_name;
2008-06-26 wenzelm 2008-06-26 added context/theory scanner;
2008-06-16 wenzelm 2008-06-16 export eof;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-01-28 wenzelm 2008-01-28 added ::: / @@@ scanner combinators;
2007-11-08 wenzelm 2007-11-08 added const_proper;
2007-11-07 wenzelm 2007-11-07 Syntax.read_typ;
2007-11-07 wenzelm 2007-11-07 removed obsolete Sign.read_tyname/const (cf. ProofContext);
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-09-01 wenzelm 2007-09-01 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-08-13 wenzelm 2007-08-13 Lexicon.read_indexname/nat/variable;
2007-07-27 wenzelm 2007-07-27 added terminator, named_attribute;
2007-05-11 wenzelm 2007-05-11 bang_facts: warning;