src/Pure/PIDE/command.ML
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned comments;
2013-07-05 wenzelm 2013-07-05 tuned signature -- eliminated pointless type synonym;
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned;
2013-07-05 wenzelm 2013-07-05 clarified type Command.eval;
2013-07-05 wenzelm 2013-07-05 tuned signature;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 wenzelm 2013-07-04 separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
2013-07-04 wenzelm 2013-07-04 more Command.memo operations; more explicit types Command.eval vs. Command.print vs. Document.exec; clarified print function parameters;
2013-07-03 wenzelm 2013-07-03 more exception handling -- make print functions total;
2013-07-03 wenzelm 2013-07-03 more print function parameters; check command_visible statically in assignment, instead of dynamically in execution;
2013-07-03 wenzelm 2013-07-03 allow multiple print functions;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-04-03 wenzelm 2013-04-03 more explicit Goal.fork_params -- avoid implicit arguments via thread data; actually fork terminal proofs in interactive mode (amending 8707df0b0255);
2013-04-03 wenzelm 2013-04-03 recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);
2013-04-02 wenzelm 2013-04-02 more centralized command timing; clarified old-style timing message;
2013-03-30 wenzelm 2013-03-30 timing status for forked diagnostic commands;
2013-02-26 wenzelm 2013-02-26 fork diagnostic commands (theory loader and PIDE interaction); explicit id for load_thy, for more robust Goal.fork accounting and commit for each theory -- NB: use_thys nodes become subject to Position.is_reported like PIDE document transactions; clarified Toplevel.command_exception vs. Toplevel.command_errors;
2013-02-24 wenzelm 2013-02-24 unified Command.is_proper in ML with Scala (see also 123be08eed88);
2013-01-16 wenzelm 2013-01-16 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16 wenzelm 2013-01-16 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-16 wenzelm 2012-10-16 more proof method text position information;
2012-08-31 wenzelm 2012-08-31 further refinement of command status, to accomodate forked proofs;
2012-08-24 wenzelm 2012-08-24 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-08-11 wenzelm 2012-08-11 vacuous execution after first malformed command;
2012-08-11 wenzelm 2012-08-11 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
2012-04-07 wenzelm 2012-04-07 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
2012-04-07 wenzelm 2012-04-07 explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
2012-04-05 wenzelm 2012-04-05 more explicit memo_eval vs. memo_result, to enforce bottom-up execution; edit of perspective touches node superficially, to ensure revisit after update;
2012-04-05 wenzelm 2012-04-05 Command.memo including physical interrupts (unlike Lazy.lazy); re-assign unstable exec, i.e. reset interrupted transaction; node result as direct exec -- avoid potential interrupt instability of Lazy.map;
2012-04-04 wenzelm 2012-04-04 separate module for prover command execution;