src/Pure/PIDE/query_operation.scala
2017-06-17 ago more permissive: avoid situations where query is silently ignored;
2017-06-16 ago more general dispatcher operations;
2017-03-12 ago tuned;
2016-12-23 ago tuned;
2016-09-05 ago clarified modules;
2015-11-02 ago avoid premature flushing and thus flashing of text area;
2015-11-02 ago clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
2015-09-21 ago support for auto update via caret focus;
2015-09-21 ago more specific name to reduce danger of clash with direct uses of plain Command.print_function;
2015-08-11 ago support hyperlinks with optional focus change;
2014-07-23 ago clarified module name: facilitate alternative GUI frameworks;
2014-04-25 ago clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
2014-04-22 ago avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-04-02 ago more explicit iterator terminology, in accordance to Scala 2.8 library;
2014-03-27 ago more careful treatment of multiple command states (eval + prints): merge content that is actually required;
2014-02-20 ago tuned imports;
2013-11-21 ago back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
2013-10-11 ago more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
2013-10-11 ago clarified Editor.current_command: allow outdated snapshot;
2013-10-07 ago clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
2013-09-25 ago explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
2013-09-24 ago skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
2013-09-24 ago tuned;
2013-08-13 ago more cleanup;
2013-08-12 ago moved generic module to its proper place;