tuned signature;

modernized setup;

tuned;

some document antiquotations for Isabelle/jEdit elements; modernized theory setup;

merged

more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges; clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);

more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;

slightly more rubust (and opportunistic) exit for old-fashioned theory_to_proof, which is used by global 'sublocale' with Named_Target.init but without proper exit;