src/Pure/PIDE/exec.ML
Thu, 11 Jul 2013 23:24:40 +0200 wenzelm more explicit type Exec.context;
Thu, 11 Jul 2013 18:41:05 +0200 wenzelm strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
Thu, 11 Jul 2013 14:42:11 +0200 wenzelm global management of command execution fragments;
less more (0) tip