more visible markup of malformed input as "bad";

tuned proofs

some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;

refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.; tuned signature;

tuned signature;

more direct Linear_Set.reverse, swapping orientation of the graph; tuned;

tuned signature;

tuned;

refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;

explicit FIXME;

tuned signature;

corrected header

refined isabelle mkroot; allow empty 'theories' to facilitate generated templates;

simplified session specifications: names are taken verbatim and current directory is default;

added build option -D: include session directory and select its sessions;