src/Pure/PIDE/command.ML
2013-07-11 ago tuned;
2013-07-10 ago print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;
2013-07-10 ago allow to remove print functions;
2013-07-10 ago clarified Command.print: update old prints here;
2013-07-09 ago more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
2013-07-08 ago more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
2013-07-05 ago tuned signature;
2013-07-05 ago tuned signature -- eliminated pointless type synonym;
2013-07-05 ago tuned signature;
2013-07-05 ago clarified type Command.eval;
2013-07-05 ago tuned signature;
2013-07-05 ago explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 ago separate exec_id assignment for Command.print states, without affecting result of eval;
2013-07-04 ago more Command.memo operations;
2013-07-03 ago more exception handling -- make print functions total;
2013-07-03 ago more print function parameters;
2013-07-03 ago allow multiple print functions;
2013-07-03 ago tuned signature;
2013-07-03 ago tuned signature;
2013-04-03 ago more explicit Goal.fork_params -- avoid implicit arguments via thread data;
2013-04-03 ago recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);
2013-04-02 ago more centralized command timing;
2013-03-30 ago timing status for forked diagnostic commands;
2013-02-26 ago fork diagnostic commands (theory loader and PIDE interaction);
2013-02-24 ago unified Command.is_proper in ML with Scala (see also 123be08eed88);
2013-01-16 ago identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16 ago more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-16 ago more proof method text position information;
2012-08-31 ago further refinement of command status, to accomodate forked proofs;
2012-08-24 ago check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-08-11 ago vacuous execution after first malformed command;
2012-08-11 ago clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
2012-04-07 ago added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
2012-04-07 ago explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
2012-04-05 ago more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
2012-04-05 ago Command.memo including physical interrupts (unlike Lazy.lazy);
2012-04-04 ago separate module for prover command execution;