more robust: provide docking framework via base plugin;

--HG--
rename : src/Tools/jEdit/src/dockable.scala => src/Tools/jEdit/src-base/dockable.scala
rename : src/Tools/jEdit/src/pide_docking_framework.scala => src/Tools/jEdit/src-base/pide_docking_framework.scala

clarified defaults;

tuned signature;

clarified modules;

clarified singleton module;

tuned;

tuned;

maintain history more often;

more uniform ComponentAdapter;

clarified tooltip;

added checkbox for try0;

clarified module name: facilitate alternative GUI frameworks;

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

more uniform Font_Info.Zoom_Box;
misc tuning and clarification;

tuned GUI;

clarified detach_operation: ignore empty output;

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;

clarified actor plumbing;

more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);

clarified tooltip_lines: HTML.encode already takes care of newline (but not space);

tuned signature -- separate module Font_Info;

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);

tuned tooltips;

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

focus text field, to capture key events even on Mac OS X look-and-feel;

focus on default component according to jEdit window management;

improved FlowLayout for wrapping of components over multiple lines;

more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;

prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;

more robust startup;

some protocol to determine provers according to ML;

eliminated pointless subgoal argument;

tuned signature -- more abstract PIDE editor operations;

tuned GUI;

more abstract consume_status operation;

more active "provers" field, which increases chances that its history is stored;

cancel_query via direct access to the exec_id of the running query process;

dockable window for Sledgehammer, based on asynchronous/parallel query operation;