src/Pure/PIDE/query_operation.ML
2016-04-09 ago clarified bootstrap;
2016-04-06 ago tuned signature;
2015-09-21 ago clarified markup;
2015-09-21 ago tuned priority (like other query operations, e.g. "find_theorems");
2015-09-21 ago tuned signature;
2015-09-21 ago separate panel for proof state output;
2015-09-21 ago more specific name to reduce danger of clash with direct uses of plain Command.print_function;
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);
2014-08-09 ago tuned comments;
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;
2013-08-12 ago clarified Query_Operation.register: avoid hard-wired parallel policy;
2013-08-10 ago explicit "strict" flag for print functions (flipped internal meaning);
2013-08-09 ago cancel_query via direct access to the exec_id of the running query process;
2013-08-09 ago clarified toplevel_error: absorb and print interrupts;
2013-08-06 ago support for query operations that consist of parallel segments;
2013-08-06 ago more explicit status for query operation;
2013-08-05 ago slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;