| Tue, 08 Apr 2014 13:24:08 +0200 | wenzelm | more precise token positions; | changeset | files |
| Tue, 08 Apr 2014 12:31:17 +0200 | wenzelm | more uniform Command.Chunk operations; | changeset | files |
| Tue, 08 Apr 2014 12:19:33 +0200 | wenzelm | more explicit Command.Chunk types, less ooddities; | changeset | files |
| Tue, 08 Apr 2014 10:24:42 +0200 | wenzelm | tuned; | changeset | files |
| 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 |