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