clarified signature;

clarified signature;

prefer control symbol antiquotations;

more embedded cartouche arguments;
more uniform LaTeX output for control symbols;

more permissive syntax;
more PIDE markup;

text antiquotation for locales (similar to classes)

--HG--
extra : rebase_source : a9383210836973a2c55c0b74c4fd6c059655c172

support rat numerals via special antiquotation syntax;

embedded content may be delimited via cartouches;

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

clarified bootstrap of @{make_string} -- avoid query on ML environment;

clarified conditional compilation;

@{make_string} is available during Pure bootstrap;

tuned;

added ML antiquotation @{method};

less confusing markup;

added @{undefined} with somewhat undefined symbol;

ML cartouches via control antiquotation;

removed obsolete undocumented feature;

formal Theory.check, with markup and completion;

@{command_spec} is superseded by @{command_keyword};

more position information and PIDE markup for command keywords;

tuned message;

semantic completion for @{system_option};

Thm.cterm_of and Thm.ctyp_of operate on local context;

added Proof_Context.cterm_of/ctyp_of convenience;

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

expand ML cartouches to Input.source;
tuned signature;

more abstract type Input.source;

added ML antiquotation @{apply n} or @{apply n(k)};

more position information, e.g. relevant for errors in generated ML source;

tuned;

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};

tuned;

added ML antiquotation @{source} for Symbol_Pos.source;

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

more uniform ML/document antiquotations;

more positions and markup;

tuned white space;

added ML antiquotation @{print};

tuned message;

clarified modules;
more antiquotations for antiquotations;