This second commit Fixes #3786.

Debugging tools used by developers have been refactored to make
them, hopefully, a bit more useful.  This is probably an ongoing
task, but this iteration is certainly better than the last!