Mon, 10 Aug 2015 16:05:41 +0200 wenzelm rendering for debugger/breakpoint active state;
Mon, 10 Aug 2015 14:14:49 +0200 wenzelm follow debugger focus;
Mon, 10 Aug 2015 14:13:49 +0200 wenzelm tuned signature;
Mon, 10 Aug 2015 13:54:12 +0200 wenzelm tuned imports;
Mon, 10 Aug 2015 11:23:49 +0200 wenzelm tuned messages;
Mon, 10 Aug 2015 11:20:16 +0200 wenzelm clarified ML options;
Sat, 08 Aug 2015 22:08:43 +0200 wenzelm merged
Sat, 08 Aug 2015 21:33:11 +0200 wenzelm more single stepping;
Sat, 08 Aug 2015 10:51:33 +0200 haftmann direct bootstrap of integer division from natural division
Thu, 06 Aug 2015 23:56:48 +0200 haftmann slight cleanup of lemmas
Thu, 06 Aug 2015 19:12:09 +0200 haftmann obsolete since no code generator without dictionary construction left
Fri, 07 Aug 2015 17:58:12 +0200 wenzelm make SML/NJ work;
Fri, 07 Aug 2015 16:15:53 +0200 wenzelm suppress empty messages as usual;
Fri, 07 Aug 2015 14:55:35 +0200 wenzelm proper Symbol.decode/encode;
Fri, 07 Aug 2015 14:46:56 +0200 wenzelm eval ML context;
Fri, 07 Aug 2015 11:44:11 +0200 wenzelm maintain history more often;
Thu, 06 Aug 2015 23:20:15 +0200 wenzelm approximate old selection after update;
Thu, 06 Aug 2015 23:08:42 +0200 wenzelm expand all rows for robustness and simplicity;
Thu, 06 Aug 2015 21:31:54 +0200 wenzelm evaluate ML expressions within debugger context;
Thu, 06 Aug 2015 20:33:12 +0200 wenzelm clarified debugger loop;
Thu, 06 Aug 2015 17:40:05 +0200 wenzelm clarified thread state;
Thu, 06 Aug 2015 14:29:05 +0200 wenzelm tuned;
Thu, 06 Aug 2015 14:28:59 +0200 wenzelm more controls;
Thu, 06 Aug 2015 14:23:59 +0200 wenzelm tuned;
Thu, 06 Aug 2015 11:46:47 +0200 wenzelm clarified signature, to make debugger.ML compile with current official ML versions;
Wed, 05 Aug 2015 21:46:52 +0200 wenzelm support for tree selection;
Wed, 05 Aug 2015 20:36:07 +0200 wenzelm proper dynamic update;
Wed, 05 Aug 2015 20:19:51 +0200 wenzelm tuned;
Wed, 05 Aug 2015 20:04:21 +0200 wenzelm more GUI components;
Wed, 05 Aug 2015 20:03:22 +0200 wenzelm tuned;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip