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;