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;
wenzelm [Thu, 27 Mar 2014 17:12:40 +0100] rev 56303
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm [Thu, 27 Mar 2014 13:00:40 +0100] rev 56302
more frugal merge of markup trees: non-overlapping tree counts as empty;
wenzelm [Thu, 27 Mar 2014 12:11:32 +0100] rev 56301
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm [Thu, 27 Mar 2014 11:19:31 +0100] rev 56300
tuned signature;
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;
wenzelm [Wed, 26 Mar 2014 21:01:09 +0100] rev 56298
tuned signature -- expose less intermediate information;
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);
wenzelm [Wed, 26 Mar 2014 20:08:07 +0100] rev 56296
less markup by default -- this is stored persistently in Isabelle/Scala;
removed dead code;
wenzelm [Wed, 26 Mar 2014 19:42:16 +0100] rev 56295
clarified valid_id: always standardize towards static command.id;