Minor issue: prjdefs.js loads a lot of information that will, most of the time, not be used. Maybe we should better get it from server.