The plugin I am now using is called “painter”. To use it, I just select a line and then press a hotkey. This adds the tags <mark class="hltr-red"> and </mark> before and after the selected line and thereby makes this line red.
Besides this way, I have also tried 1) adding the tags <font size=3, color='red'><b> and </b></font> before and after the selected line and 2) adding the tags <span style="color:red"> and </span> before and after the selected line.
All these ways successfully make the selected line red, but the latex codes in the line become unrendered (as shown in the first picture). What I am looking for is a convenient way to make a line colored like in the second picture.
