Mon, 28 Apr 2014 15:18:37 +0200 | wenzelm | more systematic delay_first discipline for change_buffer and prune_history; | changeset | files |
Mon, 28 Apr 2014 14:41:49 +0200 | wenzelm | mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later; | changeset | files |
Mon, 28 Apr 2014 14:19:14 +0200 | wenzelm | tuned; | changeset | files |
Mon, 28 Apr 2014 12:56:54 +0200 | wenzelm | added Scala version of module Event_Timer; | changeset | files |
Mon, 28 Apr 2014 00:54:31 +0200 | blanchet | restored naming trick | changeset | files |
Mon, 28 Apr 2014 00:54:30 +0200 | blanchet | more reliable 'name_of_bnf' | changeset | files |