src/Pure/Isar/outer_parse.ML
2010-03-19 wenzelm 2010-03-19 support type arguments with sort constraints;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-15 wenzelm 2010-02-15 renamed InfixName to Infix etc.;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-13 wenzelm 2009-03-13 pervasive types 'a parser and 'a context_parser;
2009-03-07 wenzelm 2009-03-07 added const_binding;
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 haftmann 2009-01-21 binding is alias for Binding.T
2009-01-02 wenzelm 2009-01-02 added type 'a parser, simplified signature; moved properties to value_parse.ML; moved props_text to isar_syn.ML;
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-19 wenzelm 2008-09-19 added props_text (from isar_syn.ML);
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements; added binding, parbinding;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-08-15 wenzelm 2008-08-15 renamed T.source_of' to T.source_position_of; tuned signature;
2008-08-14 wenzelm 2008-08-14 renamed P.ml_source to P.ML_source;
2008-08-14 wenzelm 2008-08-14 P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token; RESET_VALUE of primitive parsers; export keyword_with; renamed keyword_sid to keyword_ident_or_symbolic; added int (from args.ML); added enum(1)', and_list(1)' (formerly in args.ML); removed obsolete arguments/generic_args1 (cf. parse/parse1 in args.ML);
2008-08-07 wenzelm 2008-08-07 inner_syntax markup is back;
2008-08-07 wenzelm 2008-08-07 disabled inner_syntax markup for now;
2008-08-06 wenzelm 2008-08-06 sort/typ/term/prop: inner_syntax markup encodes original source position; added typ/term/prop_group (without inner_syntax markup);
2008-08-04 wenzelm 2008-08-04 position scanner: encode token range;
2008-06-28 wenzelm 2008-06-28 tuned args parser (cf. args.ML); tuned signature;
2008-01-28 wenzelm 2008-01-28 added ::: / @@@ scanner combinators;
2008-01-02 wenzelm 2008-01-02 added properties;
2007-12-14 wenzelm 2007-12-14 nested commands: avoid nested errors;
2007-12-05 haftmann 2007-12-05 added parser for multi_arity
2007-10-08 wenzelm 2007-10-08 avoid polymorphic equality;
2007-07-11 wenzelm 2007-07-11 replaced OuterLex.name_of by more sophisticated OuterLex.text_of;
2007-02-16 wenzelm 2007-02-16 unified arity parser/arguments;
2007-01-19 wenzelm 2007-01-19 moved parts to spec_parse.ML; tuned signature -- more exports;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-11-30 wenzelm 2006-11-30 added mixfix';
2006-11-21 wenzelm 2006-11-21 notes: proper kind;
2006-11-17 wenzelm 2006-11-17 added where_;
2006-11-14 wenzelm 2006-11-14 added for_simple_fixes, specification;
2006-11-12 wenzelm 2006-11-12 removed dead code;
2006-10-11 wenzelm 2006-10-11 added begin parser;
2006-10-11 wenzelm 2006-10-11 added opt_begin;
2006-08-01 wenzelm 2006-08-01 exported attrib;
2006-06-11 wenzelm 2006-06-11 added for_fixes;
2006-06-07 wenzelm 2006-06-07 added locale_insts;
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-17 schirmer 2006-03-17 added parser locale_expr_unless
2006-03-08 wenzelm 2006-03-08 method: goal restriction defaults to [1];
2006-03-04 wenzelm 2006-03-04 method: syntax for SelectGoals;
2006-02-10 wenzelm 2006-02-10 statement: improved error msg;
2006-02-02 wenzelm 2006-02-02 added parname; added (general_)statement (from isar_syn.ML); general_statement: Elements.statement, i.e. Shows/Obtains;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes; mixfix: added Structure;
2006-01-07 wenzelm 2006-01-07 added param, spec, named_spec;
2005-11-09 wenzelm 2005-11-09 P.context_element, P.locale_element;
2005-10-28 wenzelm 2005-10-28 syntax for literal facts;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-13 wenzelm 2005-09-13 added name_facts;
2005-08-28 wenzelm 2005-08-28 added alt_string;
2005-08-16 wenzelm 2005-08-16 added tags parser;
2005-07-07 ballarin 2005-07-07 Preparations for interpretation of locales in locales.
2005-06-20 wenzelm 2005-06-20 thmref: Name vs. NameSelection;