repaired document;

repaired document;

more markup for ML source;

merged

tuned signature;

clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";

clarified module structure;

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