type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases

more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);

more robust init;

recovered orig_text_painter from f4141da52e92;

tuned;

more elaborate syntax styles;

more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);

paint caret according to precise font metrics;

include scala mode;

builtin sub/superscript styles for jedit-4.3.2;

merged

tuned colors;

recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);

more foreground markup, using actual CSS color names;

slightly more general treatment of mutually recursive datatypes; treat datatype constructors and selectors similarly to built-in constants wrt. introduction of explicit application (in the same way as what is already done for eta-expansion)

more explicit check of dependencies;

tuned;

misc tuning and simplification;

separate module for text area painting;

improved mutabelle script to use nat for quickcheck_narrowing

quickcheck_narrowing returns some timing information

removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)

more accurate CSS colors;

some direct text foreground painting, instead of token marking; common snapshot for all text area painters (NOT gutter etc.) tuned;

imitate original Chunk.paintChunkList;

tuned;

always use our text painter;

use orig_text_painter for extras outside main text (also required to update internal line infos); tuned;

more precise imitation of original TextAreaPainter$PaintText;

tuned;

separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;

check source dependencies only if jedit_build component is available;

cover method "deepen" concisely;

moved/updated single-step tactics;

tuned sections;

reverted 5fcd0ca1f582 -- isatest provides its own libgmp3 via LD_LIBRARY_PATH, which are also required for swipl;

tuned comment

name tuning

revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug

don't trim proofs in debug mode

tuning

isatest/makedist: build Isabelle/jEdit;

makedist -j: build Isabelle/jEdit via given jedit_build component;

adding another narrowing strategy for integers

merged

pass --trim option to "eproof" script to speed up proof reconstruction

removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them

fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day

compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time

use existing ghc on macbroy20;

local gensym based on Name.variant; do not export internals by default;

uniform use of flexflex_rule;

tuned name (cf. blast_stats);

more official options blast_trace, blast_stats;

merged

merged