more permissive: avoid situations where query is silently ignored;

more general dispatcher operations;

tuned;

tuned;

clarified modules;

avoid premature flushing and thus flashing of text area;

clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);

support for auto update via caret focus;

more specific name to reduce danger of clash with direct uses of plain Command.print_function;

support hyperlinks with optional focus change;
no change of focus for debuffer position, to avoid visual glitches and keep panel active;

clarified module name: facilitate alternative GUI frameworks;

--HG--
rename : src/Pure/GUI/swing_thread.scala => src/Pure/GUI/gui_thread.scala

clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;

avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;

more explicit iterator terminology, in accordance to Scala 2.8 library;
clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics;
tuned output;

more careful treatment of multiple command states (eval + prints): merge content that is actually required;
more standard Markup_Tree merge, including trivial cases;

tuned imports;

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;
resolve sendback wrt. static command id, to allow active area even after exec_id is removed (cf. prune_delay);

more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;

clarified Editor.current_command: allow outdated snapshot;
more accurate Document_View.perspective based on current_command for proper state output (see also 88c6e630c15f and ef62204a126b);

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;

explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);

skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
tuned signature;

tuned;

moved generic module to its proper place;

--HG--
rename : src/Tools/jEdit/src/query_operation.scala => src/Pure/PIDE/query_operation.scala

more cleanup;