src/Pure/PIDE/command.scala
4 months ago ago added semantic document markers;
6 months ago ago more operations;
11 months ago ago clarified modules;
11 months ago ago clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
11 months ago ago tuned signature;
13 months ago ago less wasteful consolidation, based on PIDE front-end state and recent changes;
13 months ago ago clarified: consolidated result is last command;
13 months ago ago more node status information;
13 months ago ago clarified signature: Known.theories retains Document.Node.Entry (with header);
14 months ago ago more robust: self-export only;
14 months ago ago store exports within PIDE command state;
16 months ago ago tuned;
16 months ago ago update XML cache for slightly modified messages;
16 months ago ago more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
18 months ago ago discontinued old form of marginal comments;
20 months ago ago clarified signature;
21 months ago ago completion supports theory header imports;
23 months ago ago maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-04-20 ago tuned signature;
2017-04-17 ago tuned signature;
2017-04-03 ago provide session qualifier via resources;
2017-04-01 ago tuned signature;
2017-03-20 ago support to encode/decode command state;
2017-01-07 ago more uniform node_header (non-strict);
2017-01-07 ago tuned signature;
2017-01-07 ago tuned signature;
2017-01-05 ago suppress empty results;
2016-11-07 ago more uniform path syntax, as in ML (see 5a7c919a4ada);
2016-08-02 ago tuned signature -- prover-independence is presently theoretical;
2016-04-13 ago eliminated "xname" and variants;
2016-04-13 ago clarified syntax;
2015-11-05 ago symbolic syntax "\<comment> text";
2015-09-19 ago straight-forward refresh, without special preconditions;
2015-08-12 ago resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
2015-05-03 ago misc tuning, based on warnings by IntelliJ IDEA;
2015-04-04 ago more general notion of command span: command keyword not necessarily at start;
2015-03-17 ago misc tuning and simplification;
2015-03-16 ago avoid duplicate header errors, more precise positions;
2015-03-16 ago clarified modules;
2015-03-15 ago more markup, which helps to create missing imports;
2015-03-15 ago proper command id for inlined errors, which is important for Command.State.accumulate;
2015-03-15 ago clarified span position;
2015-03-15 ago hybrid use of command blobs: inlined errors and auxiliary files;
2015-03-15 ago tuned;
2015-03-14 ago value-oriented user error, for well-defined Thy_Syntax.chop_common;
2015-03-13 ago simplified Command.resolve_files in ML, using blobs_index from Scala;
2015-03-12 ago clarified command content;
2014-12-30 ago explicit message channel for "legacy", which is nonetheless a variant of "warning";
2014-12-01 ago tuned signature;
2014-08-12 ago tuned;
2014-08-12 ago clarified Position.Identified: do not require range from prover, default to command position;
2014-08-12 ago maintain Command_Range position as in ML;
2014-08-12 ago separate module Command_Span: mostly syntactic representation;
2014-08-11 ago tuned signature;
2014-08-11 ago tuned output, in accordance to transaction name in ML;
2014-08-11 ago more explicit type Span in Scala, according to ML version;
2014-08-02 ago more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
2014-07-23 ago more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-04-29 ago more systematic Isabelle output, like in classic Isabelle/ML (without markup);
2014-04-26 ago tuned signature;