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);
Wed, 26 Mar 2014 20:08:07 +0100 less markup by default -- this is stored persistently in Isabelle/Scala;
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;
Wed, 26 Mar 2014 19:42:16 +0100 clarified valid_id: always standardize towards static command.id;
wenzelm [Wed, 26 Mar 2014 19:42:16 +0100] rev 56295
clarified valid_id: always standardize towards static command.id;
Wed, 26 Mar 2014 14:41:52 +0100 prefer Context_Position where a context is available;
wenzelm [Wed, 26 Mar 2014 14:41:52 +0100] rev 56294
prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
Wed, 26 Mar 2014 14:15:34 +0100 unused;
wenzelm [Wed, 26 Mar 2014 14:15:34 +0100] rev 56293
unused;
Wed, 26 Mar 2014 12:32:51 +0100 more uniform Execution.fork vs. Execution.print;
wenzelm [Wed, 26 Mar 2014 12:32:51 +0100] rev 56292
more uniform Execution.fork vs. Execution.print; asynchronous Execution.fork_prints, entrusted to Execution.fork management (NB: Command.print_finished is only relevant for persistent print functions);
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip