| Tue, 08 Apr 2014 09:48:38 +0200 | wenzelm | ignore deps_changed (again) -- avoid proactive load attempts of unfinished header specification while the user is typing; | changeset | files |
| Tue, 08 Apr 2014 09:45:13 +0200 | wenzelm | no report for position singularity, notably for aux. file, especially empty one; | changeset | files |
| Mon, 07 Apr 2014 23:02:29 +0200 | wenzelm | simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name; | changeset | files |
| Mon, 07 Apr 2014 21:23:02 +0200 | wenzelm | tuned signature -- prefer static type Document.Node.Name; | changeset | files |