2014-03-01 wenzelm 2014-03-01 clarified module structure;
2014-03-01 wenzelm 2014-03-01 tuned;
2014-03-01 wenzelm 2014-03-01 tuned signature -- separate module Font_Info;
2014-03-01 wenzelm 2014-03-01 tuned;
2014-03-01 wenzelm 2014-03-01 font size change with delay, to avoid GUI lagging behind user input;
2014-03-01 wenzelm 2014-03-01 incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace); tuned signature;
2014-03-01 wenzelm 2014-03-01 more symbols, less parentheses;
2014-03-01 wenzelm 2014-03-01 tuned signature -- more explicit Document.Elements;
2014-03-01 traytel 2014-03-01 made SML/NJ happier
2014-03-01 haftmann 2014-03-01 more precise imports; avoid duplicated simp rules in fact collections; dropped redundancy
2014-03-01 haftmann 2014-03-01 earlier setup of transfer, without dependency on psychodelic interpretations
2014-03-01 haftmann 2014-03-01 cursory polishing: tuned proofs, tuned symbols, tuned headings
2014-02-28 wenzelm 2014-02-28 merged
2014-02-28 wenzelm 2014-02-28 tuned whitespace; more symbols;
2014-02-28 wenzelm 2014-02-28 allow completion within a word (or symbol), like semantic completion; no special treatment for History_Text_Field, due to lack of active range rendering;
2014-02-28 wenzelm 2014-02-28 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);
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-28 traytel 2014-02-28 made SML/NJ happier
2014-02-28 nipkow 2014-02-28 merged
2014-02-28 nipkow 2014-02-28 added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
2014-02-28 nipkow 2014-02-28 added function "List.extract"
2014-02-28 wenzelm 2014-02-28 explicit link to Z3 license;
2014-02-28 wenzelm 2014-02-28 recovered minimal README from 30de372ca56f;
2014-02-27 traytel 2014-02-27 adapt examples to new intermediate typedef
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-28 wenzelm 2014-02-28 prefer abstract datatype -- in accordance to ML version;
2014-02-28 wenzelm 2014-02-28 tuned data structure;
2014-02-28 wenzelm 2014-02-28 tuned;
2014-02-28 wenzelm 2014-02-28 tuned comment;
2014-02-28 wenzelm 2014-02-28 tuned signature;
2014-02-28 wenzelm 2014-02-28 tuned errors -- in accordance to Scala version;
2014-02-28 wenzelm 2014-02-28 tuned errors -- in accordance to ML antiquotations;
2014-02-28 wenzelm 2014-02-28 more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);
2014-02-27 wenzelm 2014-02-27 merged
2014-02-27 wenzelm 2014-02-27 tuned whitespace; tuned proofs;
2014-02-27 wenzelm 2014-02-27 tuned whitespace; modernized theory setup;
2014-02-27 wenzelm 2014-02-27 clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits; clarified asynchronous event propagation: determine buffers where they are actually accessed; tuned signature;
2014-02-27 wenzelm 2014-02-27 simplified rendering -- no need to over-emphasize "token_range";
2014-02-27 wenzelm 2014-02-27 modernized theory setup;
2014-02-27 wenzelm 2014-02-27 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;
2014-02-27 wenzelm 2014-02-27 more symbols;
2014-02-27 wenzelm 2014-02-27 more symbol abbrevs to support HOL library maintenance;
2014-02-27 wenzelm 2014-02-27 reparse only for actually changed blobs; tuned signature;
2014-02-27 wenzelm 2014-02-27 proper document blobs for initial edit, which is relevant for loading auxiliary file buffers;
2014-02-27 wenzelm 2014-02-27 more formal Document.Blobs; removed junk;
2014-02-27 wenzelm 2014-02-27 tuned output;
2014-02-27 wenzelm 2014-02-27 proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);
2014-02-27 wenzelm 2014-02-27 tuned iterator;
2014-02-27 wenzelm 2014-02-27 tuned;
2014-02-27 wenzelm 2014-02-27 tuned comment;
2014-02-26 wenzelm 2014-02-26 tuned output;
2014-02-27 haftmann 2014-02-27 amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
2014-02-27 paulson 2014-02-27 A bit of tidying up
2014-02-27 blanchet 2014-02-27 added two examples
2014-02-27 kuncar 2014-02-27 hide Lifting.invariant from a user completely
2014-02-27 blanchet 2014-02-27 correct most general type for mutual recursion when several identical types are involved
2014-02-27 Lars Hupel 2014-02-27 removed bogus "error" message (it appeared during regular mode of operation)
2014-02-26 traytel 2014-02-26 intermediate typedef for the type of the bound (local to lfp)
2014-02-26 wenzelm 2014-02-26 merged
2014-02-26 wenzelm 2014-02-26 tuned specifications and proofs;