move size hooks together, with new one preceding old one and sharing same theory data

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;

tuned spelling;

tuned menu;

NEWS;

tuned spelling;

proper signature for dynamic BeanShell action;

tuned;

added context menu for spell checker actions;

full repaint after dictionary update;

some actions to maintain spell-checker dictionary;

more explicit user declarations for main dictionary; support non-permanent declarations;

Removed old experiment (broken since b458b4ac570f resp 4159caa18f85)

added divide_nonneg_nonneg and co; made it a simp rule

support for persistent user dictionaries;

tuned;

eliminated somewhat pointless locale parameter;

tuned;

clarified complete: participate in case-mangling of check;

tuned;

added spell-checker completion dialog, without counting frequency of items due to empty name; tuned signature;

tuned signature;

special treatment for '' ligature in TeX, which counts as word separator

more elementary notion of "word" (similar to VoxSpell) -- treat hyphen as separator;

tuned rendering -- avoid overlap with squiggly underline;

added dictionaries_selector GUI; tuned;

tuned signature -- explicit Spell_Checker_Variable;

updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell; simplified dictionary file format; tuned signature;

clarified according to ML version;

merged

NEWS;

more spell_checker_elements; tuned color;

some case-mangling; clarified use of locale;

more general spell_checker_elements;

added spell-checker options; support for rendering bad words;

added bad_words; more explicit language and locale;

markup for prose words within formal comments;

added spell-checker based on jortho-1.0;

prefere standard Isabelle/Scala operation, with fixed locale;

more operations and lemmas

made mult_pos_pos a simp rule

bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced

merged

made divide_pos_pos a simp rule

fix the reflexivity prover

merged

observe also DEADID BNFs and associate the conjunction in rel_inject to the right

made ereal_add_nonneg_nonneg a simp rule

made mult_nonneg_nonneg a simp rule

merged

more formal dependencies via 'document_files';

explicit 'document_files' in session ROOT specifications; clarified Isabelle_System.copy_file(_base): preserve file-attributes and local directory hierarchy;

tuned message, to accommodate extra brackets produced by Scala parsers;

tuned;

removed obsolete doc_dump option (see also 892061142ba6);

restoring notion of primitive vs. derived operations in terms of generated code; established _paramatric suffix for parametricity rules

removed duplication and tuned

make list_all an abbreviation of pred_list - prevent duplication

add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons

simplify and fix theories thanks to 356a5efdb278

setup for Transfer and Lifting from BNF; tuned thm names