Works as expected, and makes the file editor useful

Without this plugin, the file editor is little more than a built-in notepad in a browser. With this plugin, the file editor is transformed into a useful programmer’s editor.

Why this functionality isn’t part of the core at this point, I’ll never know, but regardless, this plugin is great.

Thanks, Bryan!