clarified syntax: reject formal comments explicitly, instead of ignoring them silently;

more uniform treatment of formal comments within document source;
more robust nesting;

clarified take/drop/chop prefix/suffix;

clarified signature;

clarified signature;

scan only one line, for more detailed positions;

tuned signature;

clarified reports;
tuned signature;

tuned;

more formal treatment of control symbols;

another antiquotation short form: undecorated cartouche as alias for @{text};
document antiquotation @{text} ignores option "source";

tuned;

tuned signature;

tuned signature;

clarified control antiquotations: decode control symbol to get name;
document antiquotations @{emph}, @{bold};
symbol interpretation for \<^emph>;
tuned;

support control symbol antiquotations;

clarified Antiquote.antiq_reports;
Thy_Output.output_text: support for markdown (inactive);
eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;

trim_blanks after read, before eval;
clarified Raw_Token: uniform output_text;
tuned signature;

more markup;

clarified;

added split_lines;
tuned signature;

expand ML cartouches to Input.source;
tuned signature;

tuned signature -- prefer Input.source;

discontinued obsolete \<^sync> marker;

more markup -- complete symbols within antiquotation, notably with broken arguments;

tuned signature;

more markup;

support ML antiquotations in Scala;
tuned -- more uniform ML vs. Scala;

antiquotations within plain text: Scala version in accordance to ML;

tuned signature;

tuned -- more direct err_prefix;

cartouche within antiquotation;

discontinued unused antiquotation blocks;

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

renamed Position.str_of to Position.here;

clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);

proper error prefixes;

separate module for concrete Isabelle markup;

--HG--
rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML
rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala

bulk reports for improved message throughput;

defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);

allow nested @{antiq} (nonterminal) and @@{antiq} terminal;

more uniform variations of scan_string;

tuned signature of (Context_)Position.report variants;

datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;

export report -- version that actually covers all cases;
export check_nesting;
simplified read (again);

replaced Antiquote.is_antiq by Antiquote.is_text;

Antiquote.read: argument for reporting text;

parameterized datatype antiquote and read operation;

Antiquote.Text: keep full position information;

moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;

--HG--
rename : src/Pure/Isar/antiquote.ML => src/Pure/General/antiquote.ML