basic support for overpainting of text, imitating jEdit internals;

some support for token/chunk handling, imitating jEdit internals;

renamed thin to light, fat to heavy

code cleanup, better handling of corner cases

run blacklist algorithm only if slicing is on

implemented thin versions of "preds" type systems + fixed various issues with type args

use antiquotation

renamed "shallow" to "thin" and make it the default

more work on "shallow" encoding + adjustments to other encodings

generate type classes predicates in new "shallow" encoding

started implementing "shallow" type systems, based on ideas by Claessen et al.

added syntax for "shallow" encodings

provide isabellep as a method

append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism

tuned;

less fine-grained mira dependencies

mira hack for special settings on lxbroy10

no dependencies for Isabelle_makeall, which will be built in one go

clarified handling of ISABELLE_USEDIR_OPTIONS in mira

future merge of grammars, to improve parallel performance;

only show relevant timing;

timing of Theory_Data operations, with implicit thread positions when functor is applied;

tuned;

eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;

NEWS (cf. 4e8483cc2cc5);

simplified/unified method_setup/attribute_setup;

optional description for 'attribute_setup' and 'method_setup';

tuned signature;

merged

slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;