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;