eliminated some unused Thy_Info operations;

refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;

generic external source files -- nothing special about ML here;

discontinued special treatment of ML files -- no longer complete extensions on demand; simplified Thy_Load.check_file, with uniform error reporting; added Thy_Load.test_file for non-strict checking; misc tuning and simplification;