allow registration of custom size functions for BNF-based datatypes

reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'

generate 'rec_o_map' and 'size_o_map' in size extension

made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)

generate size instances for new-style datatypes

invoke 'fp_sugar' interpretation hook on mutually recursive clique

declare 'bool' and its proxies as a datatype for SPASS-Pirate

added 'inj_map' as auxiliary BNF theorem

tuned whitespace

remove add_eq_zero_iff, it is replaced by add_nonneg_eq_0_iff; also removes it from the simpset

favorites for jEdit file browser, although an expanded directory path is expected here, not environment variables;

tuned;

clarified exit code for the rare situation where Runtime.exn_error_message might fail;

tuned;

tuned -- avoid warning about catch-all handler;

more general exit;

swap with qualifier; tuned

sos accepts False, returns apply command

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

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;

tuned signature -- separate module Word;

more NEWS;

tuned default: melange of all "en" dialects;

updated to jortho-1.0-2: added dictionary "en-CA", changed dictionary "en" to be the union of all dialects instead of intersection;

more context-sensitivity;

tuned spelling;

back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);

prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing; more robust point_range; tuned;

clarified abbreviations for cartouche delimiters, to work in any context;

clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;

more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;

avoid conflict of Isabelle/jEdit popups with jEdit context menu;

clarified before_caret_range: prevent continuation on next line; more robust jedit_text_areas in unclear situations of object initialization;

explicit menu action to complete word;

common context menu for Isabelle/jEdit;

tuned;

tuned;