warn users about unused "using" facts

be less aggressive at kicking out chained facts

recognize bus errors as crash

consider removing chained facts last, so that they're more likely to be kept

clarified format of etc/options: only declarations, not re-definitions;

check_errors for cumulative session content;

even more defensive path expansion (see also 8d381fdef898);

support for 'typ' with explicit sort constraint;

added jedit option -d;

always retain doc-src (as regular component);

merged

Calling isabelle with proper (relative) path, no longer relying on $PATH.

fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;

updated to jedit-4.5.2 (still unchanged);

restored ISABELLE_OUTPUT etc -- still relevant at least for mira.py itself

tuned;

fixed mira.py (cf. fd50596bf78b)

more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;

more static antiquotations;

always show some timing information, to reduce the need for explicit -v;

some information for central Isabelle repository configuration;

reduced settings patching

removed obsolete configuration AFP_images

faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;

simplified symbol matching;

further clarification of malformed symbols;

more liberal scanning of potentially malformed symbols;

vacuous execution after first malformed command;

clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;

tuned markup;

tuned message;

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

reports with body text, not just markup;

fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end

special code with lists no longer necessary, use sets

proper error prefixes;

more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;

tuned message;

clarified Linear_Set.next/prev: check definedness;

merged

Improved complete lattice formalisation - no more index set.

merged

tuned proofs;

sneak message into "bad" markup as property -- to be displayed after YXML parsing;

apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.; expand Clear edit before sending to prover; at most one full reparse of each node;

clarified undefined, unparsed, unfinished command spans; common reparse_spans, diff_commands; some support for consolidate_spans after change of perspective;

tuned;

discontinued mostly unused markup for command spans;