hide Lifting.invariant from a user completely

correct most general type for mutual recursion when several identical types are involved

removed bogus "error" message (it appeared during regular mode of operation)

intermediate typedef for the type of the bound (local to lfp)

merged

tuned specifications and proofs;

more precise before_caret_range (looking both in space and time);

improved rendering of blinking cursor;

markup for method combinators;

tuned;

tuned signature;

suppress completion of obscure keyword, avoid confusion with plain "simp";

method language markup, e.g. relevant to prevent outer keyword completion;

transfer domain rule for special case of functions - was missing

replaced smt-based proof with metis proof that requires no external tool

obsolete workaround

prefer proof context over background theory

made tactics more robust

merged

tuned specifications and proofs;

merged

uniform insert vs. popup policy;

tuned proofs;

back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;

tuned signature;

no word completion within word context;

more completion rendering: active, semantic, syntactic; tuned;

tuned;