| Thu, 27 Feb 2014 21:36:40 +0100 | wenzelm | merged | changeset | files |
| Thu, 27 Feb 2014 21:31:58 +0100 | wenzelm | tuned whitespace; | changeset | files |
| Thu, 27 Feb 2014 21:27:58 +0100 | wenzelm | tuned whitespace; | changeset | files |
| Thu, 27 Feb 2014 21:02:09 +0100 | wenzelm | 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; | changeset | files |
| Thu, 27 Feb 2014 17:56:59 +0100 | wenzelm | simplified rendering -- no need to over-emphasize "token_range"; | changeset | files |
| Thu, 27 Feb 2014 17:39:20 +0100 | wenzelm | modernized theory setup; | changeset | files |
| Thu, 27 Feb 2014 17:29:58 +0100 | wenzelm | store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; | changeset | files |