It would be great if students could use the editor with the indentation width they’re used to from their regular text editors.

In case you implemented actual tab characters, you could just set a CSS property (“tab-size”) which controls how wide one tab should be, which would also fix #535 without any over-engineered algorithms. ;)

Submitted on 18 November 2016 at 07:37