| 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 |