| Sat, 02 Jun 2018 22:39:45 +0200 | wenzelm | more symbols; | changeset | files |
| Sat, 02 Jun 2018 22:14:35 +0200 | wenzelm | more formal comments; | changeset | files |
| Sat, 02 Jun 2018 22:11:09 +0200 | wenzelm | more args; | changeset | files |
| Sat, 02 Jun 2018 21:59:11 +0200 | wenzelm | record active execution task and depend on it -- avoid new executions bumping into old ones; | changeset | files |
| Sat, 02 Jun 2018 21:10:20 +0200 | wenzelm | tuned -- more explicit types; | changeset | files |
| Sat, 02 Jun 2018 19:52:16 +0200 | wenzelm | less frequent consolidation: it requires a full Document.update and Document.start_execution; | changeset | files |