tuned;

tuned signature -- separate module Font_Info;

tuned;

font size change with delay, to avoid GUI lagging behind user input;

incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace); tuned signature;

more symbols, less parentheses;

tuned signature -- more explicit Document.Elements;

made SML/NJ happier

more precise imports; avoid duplicated simp rules in fact collections; dropped redundancy

earlier setup of transfer, without dependency on psychodelic interpretations

cursory polishing: tuned proofs, tuned symbols, tuned headings

merged

tuned whitespace; more symbols;

allow completion within a word (or symbol), like semantic completion; no special treatment for History_Text_Field, due to lack of active range rendering;

more regular buffer_range, despite 47e8c8daccae; more robust invalidate_range, which is relevant when editing at the end of the buffer (NB: last line offset by be outside actual buffer length);

load Metis a little later

made SML/NJ happier

merged

added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets

added function "List.extract"

explicit link to Z3 license;

recovered minimal README from 30de372ca56f;

adapt examples to new intermediate typedef

joint work with blanchet: intermediate typedef for the input to fp-operations