Thu, 27 Mar 2014 19:47:30 +0100 back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);
wenzelm [Thu, 27 Mar 2014 19:47:30 +0100] rev 56306
back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);
Thu, 27 Mar 2014 18:42:53 +0100 tuned;
wenzelm [Thu, 27 Mar 2014 18:42:53 +0100] rev 56305
tuned;
Thu, 27 Mar 2014 17:56:13 +0100 redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm [Thu, 27 Mar 2014 17:56:13 +0100] rev 56304
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;
Thu, 27 Mar 2014 17:12:40 +0100 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm [Thu, 27 Mar 2014 17:12:40 +0100] rev 56303
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
Thu, 27 Mar 2014 13:00:40 +0100 more frugal merge of markup trees: non-overlapping tree counts as empty;
wenzelm [Thu, 27 Mar 2014 13:00:40 +0100] rev 56302
more frugal merge of markup trees: non-overlapping tree counts as empty;
Thu, 27 Mar 2014 12:11:32 +0100 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm [Thu, 27 Mar 2014 12:11:32 +0100] rev 56301
more frugal merge of markup trees: filter wrt. subsequent query;
Thu, 27 Mar 2014 11:19:31 +0100 tuned signature;
wenzelm [Thu, 27 Mar 2014 11:19:31 +0100] rev 56300
tuned signature;
Thu, 27 Mar 2014 10:43:43 +0100 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm [Thu, 27 Mar 2014 10:43:43 +0100] rev 56299
more careful treatment of multiple command states (eval + prints): merge content that is actually required; more standard Markup_Tree merge, including trivial cases;
Wed, 26 Mar 2014 21:01:09 +0100 tuned signature -- expose less intermediate information;
wenzelm [Wed, 26 Mar 2014 21:01:09 +0100] rev 56298
tuned signature -- expose less intermediate information;
Wed, 26 Mar 2014 20:32:15 +0100 support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm [Wed, 26 Mar 2014 20:32:15 +0100] rev 56297
support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip