Document_View: some markup for main inner syntax categories;

Command.State.accumulate: check actual source range;

Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;

highlight bad range of nested error (here from inner parsing);

Isar_Document.reported_positions: exclude proof state output;

Document_View: less aggressive background coloring, departing from classic PG highlighting; tuned colors;

report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase; tuned color;

slightly more robust Plugin.stop -- components might refer to Isabelle.system even after shutdown;

turned show_hyps and show_tags into proper configuration option;

discontinued obsolete ProofContext.prems_limit; simplified command setup for 'pr' etc.;

ML_Context.thm and ML_Context.thms no longer pervasive;

more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;