embedded content may be delimited via cartouches;

clarified type Token.src: plain token list, with usual implicit value assignment;
clarified type Token.name_value, notably for head of Token.src;
clarified Attrib/Method check_src vs. parser;

tuned signature;

tuned signature;

tuned signature;

clarified Token.check_src: intern at most once;
Method.parse_internal for Eisbach: intern method names;

cartouche_declaration for Eisbach;

more abstract type Input.source;

support for declaration within token source;

support for nested Token.src within Token.T;
tuned signature;

tuned signature -- moved type src to Token, without aliases;

more informative Token.Name with history of morphisms;
tuned signature;

more informative Token.Fact: retain name of dynamic fact (without selection);

proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);

allow text cartouches in regular outer syntax categories "text" and "altstring";

support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;

more markup for improper elements;

tuned signature;

unused;

more explicit markup for Token.Literal;
Markup.quasi_keyword for Parse.$$$ -- it is used within Args.syntax as well;
Markup.operator for name of Args.syntax, to override outer keywords like "where";
tuned signature;

tuned messages -- in accordance to Isabelle/Scala;

tuned;

proper Args.syntax for slightly odd bundle trickery;
do not handle arbitrary exceptions;
more abstract type Args.src;

more markup;

clarified Args.check_src: retain name space information for error output;
tuned signature;

clarified Args.src: more abstract type, position refers to name only;
prefer self-contained Args.check_src;

tuned signature;

prefer Name_Space.pretty with its builtin markup;

tuned signature;

modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
proper context for global data;
tuned signature;

reject internal term names outright, and complete consts instead;
more general Name_Space.check_reports;
more compact Markup.markup_report;

eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);

more uniform check_const/read_const;

tuned signature -- more uniform check_type_name/read_type_name;
proper reports for read_type_name (lost in 710bc66f432c);

suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
tuned signature;

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 ":", "|", "?";

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";

tuned message -- more markup;

tuned signature;

tuned message;

tuned signature;

tuned signature;

cartouche within nested args (attributes, methods, etc.);

support for nested text cartouches;
clarified Symbol.is_symbolic: exclude \<open> and \<close>;

tuned signature;

more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;

proper exhaustive match (cf. e9beabf045ab);

renamed Position.str_of to Position.here;

tuned signature -- refined terminology;

tuned Parse.group: delayed failure message;

proper binding/report of defined simprocs;
tuned signature;

modernized structure Proof_Context;

support for real valued configuration options;

renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
eliminated slightly odd alias structure T;

--HG--
rename : src/Pure/Isar/outer_lex.ML => src/Pure/Isar/token.ML

refer directly to structure Keyword and Parse;
eliminated old-style structure aliases K and P;

ProofContext.read_const: allow for type constraint (for fixed variable);
added proof command 'write' to introduce concrete syntax within a proof body;

removed unused Args.maxidx_values and Element.generalize_facts;

eliminated Args.bang_facts (legacy feature);

clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;

clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;

fixed spelling;

bang_facts: legacy feature;

eliminated redundant bindings;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

de-camelized Symbol_Pos;

simplified goal_spec: default to first goal;

eliminated type Args.T;
pervasive types 'a parser and 'a context_parser;

Assumption.all_prems_of, Assumption.all_assms_of;

Merge.

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;

removed Ids;

binding is alias for Binding.T

cleaned up binding module and related code

new Binding module

added binding;
thm_name/opt_thm_name: Name.binding;

Args.name_source(_position) for proper position information;

pass token source to typ/term etc.;

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);

abstract type Scan.stopper;

tuned nested args parser;
export generic_args1;

added thm_name, opt_thm_name;

added context/theory scanner;

export eof;

renamed datatype thmref to Facts.ref, tuned interfaces;

added ::: / @@@ scanner combinators;

added const_proper;

Syntax.read_typ;

removed obsolete Sign.read_tyname/const (cf. ProofContext);

generic Syntax.pretty/string_of operations;

replaced ProofContext.read_term/prop by general Syntax.read_term/prop;

Lexicon.read_indexname/nat/variable;

added terminator, named_attribute;

bang_facts: warning;

Morphism.transform/form;

Morphism.fact;

switched argument order in *.syntax lifters

added term_abbrev;

tuned pretty_src output;

attribute value: morphism;

renamed Name value to Text, which is *not* a name in terms of morphisms;

replaced map_values by morph_values;

moved pretty_attribs to attrib.ML;

member (op =);

normalized Proof.context/method type aliases;

added maxidx_values;

moved basic assumption operations from structure ProofContext to Assumption;

query/bang_colon: separate tokens;

tuned basic list operators (flat, maps, map_filter);

Context.generic is canonical state of parsers;
removed obsolete global/local parsers;
tuned interfaces;

simplified type attribute;

added generic syntax;
mk_attribute: generic;

syntax for literal facts;

removed obsolete Theory.sign_of;

added liberal_name;

renamed global/local_typ_raw to global/local_typ_abbrev;

added symbol scanner;

Syntax.read_variable;

*** MESSAGE REFERS TO PREVIOUS VERSION ***
support embedded values and static binding -- via implicit assignment
to src tokens (cf. assignable/assign/closure);
renamed ident/string/keyword to mk_ident/mk_string/mk_keyword;
added mk_name, mk_typ, mk_term, mk_fact, mk_attribute;
added type value with map_values etc.;
removed name_dummy, added general 'maybe' combinator;
added global/local_tyname/const;
added pretty_src, pretty_attribs;
added thm_sel (from attrib.ML);

*** empty log message ***

First version of global registration command.

Move towards standard functions.

Deleted Library.option type.

Merged in license change from Isabelle2004

do *not* export list/list1 -- commas considered special in arg syntax;

xxx_typ_raw replace xxx_typ_no_norm forms;

the function list1 has been exported.

change quote to Library.quote, fixes LaTeX \isarchardoublequote problem.

tuned;

Methods rule_tac etc support static (Isar) contexts.

tuned error message;

added "bracks";

added common args keywords;

Args.addN, Args.delN;

avoid handle_error (better msgs);

added mode parser;

added string_of;

added int;

typ_no_norm;

removed obsolete "{}";

replaced {{ }} by { };

GPLed;
added colon, parens;

Args.name_dummy;

goal_spec: [!];

goal_spec;

tuned syntax wrapper;

attrib: keyword_symid;
goal_spec;

removed pats;

added bang_facts;

lifted enum;
removed list(1);
added and_list(1);

term_pat vs. prop_pat;

removed trace;

several args parsers;
include positions;
misc tuning;

Concrete argument syntax (for attributes, methods etc.).