src/Pure/PIDE/command.ML
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;
2014-12-09 ago imitate command markup and rendering of Isabelle/jEdit in HTML output;
2014-11-26 ago renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 ago prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-11-06 ago more explicit Keyword.keywords;
2014-11-01 ago tuned signature, in accordance to Scala version;
2014-10-31 ago discontinued obsolete control command category;
2014-08-12 ago separate module Command_Span: mostly syntactic representation;
2014-08-02 ago more emphatic warning via error_message (violating historic TTY protocol);
2014-08-01 ago prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
2014-05-13 ago no reset for 'end' -- e.g. relevant for 'notepad';
2014-05-12 ago smarter recovery from toplevel type error;
2014-05-07 ago run commands as interactive, again after long history of fluctuation (9e196062bf88, 173974e07dea, e07dacec79e7) and quite different infrastructure for print tasks;
2014-05-07 ago discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
2014-05-06 ago clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
2014-05-06 ago explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
2014-04-10 ago tuned error -- allow user to click on hyperlink to open remote file;
2014-04-07 ago simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
2014-04-07 ago separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
2014-03-31 ago support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-26 ago more uniform Execution.fork vs. Execution.print;
2014-03-26 ago added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
2014-03-24 ago discontinued Toplevel.debug in favour of system option "exception_trace";
2014-03-10 ago some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
2014-02-28 ago tuned signature;
2014-02-27 ago store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
2014-02-24 ago clarified Token.range_of in accordance to Symbol_Pos.range;
2014-02-24 ago tuned signature;
2014-02-11 ago report (but ignore) markup within auxiliary files;
2013-12-05 ago more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
2013-12-05 ago merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
2013-11-28 ago more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
2013-11-25 ago more defensive order of Markup.failed vs. Markup.finished -- more informative status in Isabelle/Scala, although it is not rendered in Isabelle/jEdit;