src/Pure/PIDE/command.ML
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;