How come this.__proto__ being deprecated but Object.getPrototypeOf(this) not implemented?

I liked __proto__ too, but it does feel a bit hacky :) I'll add an issue for sticking getPrototypeOf in.

the reference list is exhaustive, right?

Yep, it's whatever is in the current release of Espruino, so at the moment 1v85. There may be some other stuff in the latest Git build.

about what is ultimately feed to the linter...

@allObjects - https://github.com/espruino/EspruinoWebIDE/blob/gh-pages/js/core/editorJavaScript.js#L29 :)

I'm not sure it needs to be configurable, but disabling just that warning should be easy.