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

removed odd context argument: Thy_Info.get_theory does not fit into PIDE document model;

obsolete for release;

obsolete since polyml-5.5.0;

added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;

reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);

added protocol command "use_theories", with core functionality of batch build;

tuned comments;

tuned;

tuned option name;

tuned;

proper tooltip_lines for multi-line text;

unused;

capitalize more carefully, e.g. relevant for option "ML_exception_trace";

more simp rules for Fun.swap

updated to jdk-8u5;

avoid ooddity: invoke intended function instead of java.awt.Container.invalidate();

tuned;

tuned spelling;

more uniform treatment of word case for check / complete;

capitalize fully (like in Emacs);

clarified word case; more robust treatment of codepoints;

more specific support for sequence of words;