Highlight consumed input

[winniederidder]

This PR adds support for highlighting the lines that have been consumed in batch mode.
A div element with contenteditable=true has some undesirable default behaviour that is very clunky and error-prone to work with (first child is a TextNode before using divs, replacing that TextNode with a div causes new elements to appear, ...) so I decided to stop using it. Instead, CodeMirror already provides an editor with plenty of flexiblity and a useful API. This editor can then share some code with the CodeEditor-class.

To provide actual highlighting and gutters, I added new classes. The Gutters base class allows creating arbitrary gutters (such as the checkmark gutter, but also a breakpoint gutter (useful for #109)). To prevent code duplication in the BatchInputEditor, I created a base class grouping similar functionality between the input and the code editor together. I also used the CodeMirror theme extension to properly fix the layout of the editor is always correct.

The highlight-style is still up for debate. I currently use the built-in CodeMirror activeLine classes.

Closes #82
Depends on #216 (to be able to use cleaned version of onChange in the new Editor base class)

[winniederidder]

Older discussions can be found on #196

[bmesuere]

Can this be deployed somewhere? https://papyros.dodona.be/dev shows a blank page for me.

[winniederidder]

Can this be deployed somewhere? https://papyros.dodona.be/dev shows a blank page for me.

I didn't get a blank page, but I have also scheduled a deployment as the deployed version wasn't this one.
Deploying is done manually under Actions > Deploy GitHub pages, as there was an issue with allowing both manual deployments and triggering on adding labels.

[bmesuere]

• I had to manually uninstall the service worker through devtools to get this to load on /dev
• The gutter is very narrow, can you add some padding left and right of the icon?
• I don't think the green color is needed
• Can we somehow highlight the next line to be used as "active" using a light bg-color?
• Tooltip: "This line has already been used as input", "Deze regel werd al gebruikt als invoer"
• There seems to be a slight misalignment between the editor and gutter (both code and input). The vertical alignment of the gutter is off, you can easily see this for highlighted lines:
  

[winniederidder]

• I had to manually uninstall the service worker through devtools to get this to load on /dev

That's odd. The service worker hasn't been changed in quite a while, so I'm unsure what could cause this issue.

[winniederidder]

• Tooltip: "This line has already been used as input", "Deze regel werd al gebruikt als invoer"

Does this mean the part containing the prompt it answered should be omitted? Or should I append that to these strings?

[pdawyndt]

@winniederidder: The version that is deplyoyed right now on /dev, doesn't seem to have the latest changes when it comes to input lines that have already been processed (marking those lines, tooltip of icon, making the line read-only). On Windows 10 / Chrome I haven't seen anything that needed to be done to make the service workers work (at least not recently).

[winniederidder]

@winniederidder: The version that is deplyoyed right now on /dev, doesn't seem to have the latest changes when it comes to input lines that have already been processed (marking those lines, tooltip of icon, making the line read-only). On Windows 10 / Chrome I haven't seen anything that needed to be done to make the service workers work (at least not recently).

Correct, I re-deployed the run-python-doctest branch so that @bmesuere can review that branch more easily, as I applied the suggested changes.

[winniederidder]

After applying the suggestions and fixing some other issues, this is the current state:

Layout likely still needs tweaking. Currently a cyan background is used for consumed lines, and a light background is applied to the line that will be used.

[pdawyndt]

Highlighting line that will be consumed next is a bit weird as a feature, as there is no guarantee that another line will be consumed. On the other side, the highligting is so subtle that almost need to know this feature exists, to notice it.

[pdawyndt]

Just as the code in the editor is stored and reused after a page load, it might be interesting to do the same for batch input.

[pdawyndt]

Chan background color doesn’t look great in dark mode.

[pdawyndt]

Misalignment between editor and gutter now even seems worse. Hadn’t noticed it myself before, but now I clearly see it on iPad.

[pdawyndt]

Would be better if the gutter got a distinct color in dark mode (as it has in light mode), otherwise it might seem as if the batch input editor has a left margin that is too broad.

[winniederidder]

Misalignment between editor and gutter now even seems worse. Hadn’t noticed it myself before, but now I clearly see it on iPad.

So, after the recent changes it is visible on iPad yet better on the desktop version?

[winniederidder]

@bmesuere @pdawyndt I should have resolved the given remarks and deployed the newest version.
Last issue is likely the styling of the consumed and next-to-use lines (see the comment from Peter).