wenzelm [Fri, 03 Sep 2010 21:13:53 +0200] rev 39371
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm [Fri, 03 Sep 2010 20:39:38 +0200] rev 39370
tuned comment;
wenzelm [Fri, 03 Sep 2010 18:03:48 +0200] rev 39369
merged
wenzelm [Fri, 03 Sep 2010 17:57:12 +0200] rev 39368
modernized session ROOT;
wenzelm [Fri, 03 Sep 2010 17:54:43 +0200] rev 39367
disposed left-over user preferences;
wenzelm [Fri, 03 Sep 2010 17:43:44 +0200] rev 39366
turned show_all_types into proper configuration option;
wenzelm [Fri, 03 Sep 2010 16:36:33 +0200] rev 39365
treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;
wenzelm [Fri, 03 Sep 2010 16:09:12 +0200] rev 39364
more explicit Config.declare vs. Config.declare_global;
wenzelm [Fri, 03 Sep 2010 15:54:03 +0200] rev 39363
turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
haftmann [Fri, 03 Sep 2010 16:08:19 +0200] rev 39362
merged