clarified kill on Windows: just one executable;

avoid deprecated PluginOptions with its unbounded window size;

clarified undefined_blobs: already loaded theories are suppressed; enabled jedit_auto_resolve (again): e.g. relevant for debugging when following links through source files;

tuned spacing

tuned exercise

merged

reset focus after thread update (with new debug_states);

atomic Debugger.status; output without thread context is empty; tuned;

tuned;

tuned;