tuned signature;

prefer control symbol antiquotations;

more markup for HTML rendering;

embedded content may be delimited via cartouches;

simplified default print_depth: context is usually available, in contrast to 0d295e339f52;

clarified modules -- simplified bootstrap;

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;

more careful handling of auxiliary environment structure -- allow nested ML evaluation;

expand ML cartouches to Input.source;
tuned signature;

clarified syntax -- avoid overlap with command category;

tuned signature;

tuned whitespace;

tuned signature -- define some elementary operations earlier;

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

redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
more explicit ML_Compiler.flags;

added command 'SML_file' for Standard ML without Isabelle/ML add-ons;

clarified modules;
more antiquotations for antiquotations;

tuned signature -- rearranged modules;

tuned signature -- clarified module name;

--HG--
rename : src/Pure/ML/ml_antiquote.ML => src/Pure/ML/ml_antiquotation.ML

simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
added command 'print_ML_antiquotations';

modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
proper context for global data;
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 ":", "|", "?";

more explicit method reports;
avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);

tuned;

method language markup, e.g. relevant to prevent outer keyword completion;

prefer user-space tool within Pure.thy;

more markup;

tuned signature;

proper context for norm_hhf and derived operations;
clarified tool context in some boundary cases;

added Theory.setup convenience;

clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);

tuned signature;

tuned;

more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;

faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;

clarified signature;

added ML antiquotation @{attributes};

proper source positions for @{lemma};

ML antiquotations are managed as theory data, with proper name space and entity markup;
clarified Name_Space.check;

modernized structure Proof_Context;

reverted 08240feb69c7 -- breaks positions of reports;

more robust ML antiquotations -- allow original tokens without adjacent whitespace;

modernized some structure names, keeping a few legacy aliases;

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

modernized naming conventions of main Isar proof elements;

simplified interface for ML antiquotations, struct_name is always "Isabelle";

eliminated obsolete thm position tags;

adapted Generic_Data, Proof_Data;
tuned;

ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;

removed Ids;

ML_Context.add_antiq: pass position;
@{lemma}: set source position;

unified Args.T with OuterLex.token, renamed some operations;

@{lemma}: allow terminal method, close derivation unless (open) mode is given;

Isar theorem values within ML.