re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;

explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);

tuned

eliminate duplicated constant (diag vs. Id_on)

hide internal constants; tuned proofs

tuned

tuned

added advanced rule induction subsection

merged

more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;