tuned data structures

tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge; n. b. merging of bidirectional dependencies results in effective join of involved nodes: no termination problem since ancestry is always kept explicitly normalized

tuned

tuned names

eta-expand all search patterns using schematic place holders

revert "better" handling of abbreviation from c61fe520602b

tuned variable names

turn application-specific Pattern.matches_subterm into an application-private function

cleaned up mess

add Poisson and Binomial distribution

add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav

proper GUI_Thread context (cf. 7e0d3da6e6d8);

more examples;

tuned header;

generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces

merged

node-specific keywords, with session base syntax as default;

clarified define_command: send tokens more directly, without requiring keywords in ML;

more robust bundle_name: avoid assumptions about identifier, keywords etc.;

tuned signature;

tuned;

clarified token kind;

added Untyped.method convenience (for *this* class only);

tuned signature -- more explicit types;

more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;

node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;

clarified token marker / syntax for mode vs. buffer;

Sidekick syntax is derived from buffer (and its mode), instead of parser name;

tuned signature;

more merge operations;