src/Pure/PIDE/query_operation.ML
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;