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

prefer abstract datatype -- in accordance to ML version;

tuned data structure;

tuned;

tuned comment;

tuned signature;

tuned errors -- in accordance to Scala version;

tuned errors -- in accordance to ML antiquotations;

more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);

merged

tuned whitespace; tuned proofs;