src/Pure/PIDE/query_operation.ML
2014-08-09 wenzelm 2014-08-09 tuned comments;
2014-03-31 wenzelm 2014-03-31 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 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2013-08-12 wenzelm 2013-08-12 clarified Query_Operation.register: avoid hard-wired parallel policy; sledgehammer: more conventional parallel exception handling -- print just one interrupt;
2013-08-10 wenzelm 2013-08-10 explicit "strict" flag for print functions (flipped internal meaning); non-strict query operations may operate on failed states;
2013-08-09 wenzelm 2013-08-09 cancel_query via direct access to the exec_id of the running query process;
2013-08-09 wenzelm 2013-08-09 clarified toplevel_error: absorb and print interrupts; tuned;
2013-08-06 wenzelm 2013-08-06 support for query operations that consist of parallel segments;
2013-08-06 wenzelm 2013-08-06 more explicit status for query operation; avoid output with outdated snapshot; animation rate according to status; added PIDE.document_snapshot convenience -- independent of availability of physical buffer;
2013-08-05 wenzelm 2013-08-05 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;