more uniform treatment of "keyword" vs. "operator";

simplified Line_Context (again);

more robust treatment of partial range restriction;

select_markup: no filtering here -- results may be distorted anyway;

more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;

more explicit error message; convert/revert range; tuned;

merged

gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"

added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users

fixed soundness bug related to extensionality

unconditional recovery from bad context (e.g. Quoted with malformed quoted_body);

flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);

recovered markup for non-alphabetic keywords;

more precise imitation of original TextAreaPainter: no locking;

more precise imitatation of original TokenMarker: no locking, interned context etc.;

brute-force range restriction to avoid spurious crashes;

static token markup, based on outer syntax only; eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.);

explicit dependency on Pure.jar;

partial scans of nested comments;

some support for partial scans with explicit context; clarified junk vs. junk1;

tuned spelling

updated generated file;

merged

spelling

avoid compiler warning -- this is unchecked anyway;

tuned messages;

uniform use of Document_View.robust_body;

merged

merge

fixed soundness bug made more visible by previous change

use more appropriate type systems for ATP exporter

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;