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