src/Pure/PIDE/command.ML
4 months ago ago added semantic document markers;
4 months ago ago clarified signature;
4 months ago ago clarified Toplevel.state: more explicit types;
4 months ago ago physical vs. logical events, the latter takes GC time into account;
6 months ago ago {* verbatim *} is explicit legacy feature;
10 months ago ago proper tast_context (amending 5f44ad150ed8);
10 months ago ago more robust: avoid race-condition of terminated vs. consolidated;
10 months ago ago clarified quasi_consolidated state: ensure that exports are present for ok nodes;
10 months ago ago more robust reset_state: begin/end structure takes precedence over goal/proof structure;
10 months ago ago tuned;
10 months ago ago more explicit status for "canceled" command within theory node;
10 months ago ago more robust: memoize interrupt (e.g. resource problem) -- avoid multiple attempts;
10 months ago ago more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
10 months ago ago more accurate position for auxiliary files;
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 fork parallel prints early in execution: avoid degradation of priority due to main eval task;
13 months ago ago clarified priority;
13 months ago ago support for anonymous print function values;
13 months ago ago tuned;
14 months ago ago support for dynamic document output while editing;
14 months ago ago clarified future scheduling parameters, with support for parallel_limit;
17 months ago ago just one check of formal comments;
17 months ago ago avoid proliferation of language_document reports;
17 months ago ago clarified take/drop/chop prefix/suffix;
18 months ago ago discontinued old form of marginal comments;
18 months ago ago theory Pure is default presentation context;
18 months ago ago check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
19 months ago ago positions as postlude: avoid intrusion of odd %-forms into main tex source;
19 months ago ago simplified positions -- line is also human-readable in generated .tex file;
19 months ago ago more robust range on preceding comment-line;
23 months ago ago maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-06-22 ago more informative task_statistics;
2017-05-27 ago clarified build errors;
2016-12-28 ago more uniform treatment of "bad" like other messages (with serial number);
2016-07-13 ago obsolete;
2016-07-13 ago semantic indentation for unstructured proof scripts;
2016-04-09 ago tuned signature -- closer to Exn.Interrupt.expose in Scala;
2016-04-06 ago treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
2016-04-02 ago prefer infix operations;
2016-03-03 ago clarified modules;
2015-10-16 ago clarified Antiquote.antiq_reports;
2015-10-09 ago more direct HTML presentation, without print mode;
2015-09-21 ago option editor_output_state;
2015-09-21 ago separate panel for proof state output;
2015-06-29 ago improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-04-16 ago more explicit bootstrap_thy;
2015-04-15 ago tuned messages;
2015-04-12 ago clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
2015-04-07 ago recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;
2015-03-25 ago tuned signature;
2015-03-13 ago simplified Command.resolve_files in ML, using blobs_index from Scala;
2015-03-12 ago clarified markup for embedded files, early before execution;
2015-01-29 ago discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
2015-01-29 ago ensure that running into older execution is interruptible (see also b91dc7ab3464);
2015-01-11 ago do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);
2015-01-09 ago non-strict print_state: display old proof state on failure, e.g. unfinished command;
2015-01-09 ago ignore print process even after fork, to avoid loosing active worker threads;
2014-12-28 ago eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
2014-12-27 ago memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;