back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;

recovered outdated_color (cf. 4beb2f41ed93);

more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;

tuned proofs;

tuned

tuned signature;

comments;

tuned proofs;

eliminated dead code, together with spurious warning about congruence rule for "Fun.comp";

more explicit/robust treatment of common snapshot;

discontinued old-style Term.list_abs in favour of plain Term.abs;

renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;

renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;

tuned;

discontinued old-style Term.list_all_free in favour of plain Logic.all;

tuned;

discontinued default rendering for Oheimb's double-space;

tuned white space;

tuned comment;

paranoia null check -- prevent spurious crash of jedit token markup;

tuned comments;

tuned signature;

clarified partial restrict operation;

tuned proofs;

ignore empty gfx_range; tuned;

tuned signature;

tuned

handle specific exception, not arbitrary ones (including Interrupt);

eliminated dead code;

more modest settings for lxbroy10 -- might actually perform better;