A setting to disable showing Coq response on mouse hover

[anton-trunov]

Hi, I noticed that when presenting material in a class I tend to select some piece of text/code with my mouse, and when doing so the cursor tends to cross a lot of lines and the popup window blinks a lot which might distract the audience.

Having a checkbox that lets us opt out of the default "pop up on mouse hover" behavior seems to be an easy solution. Would that be a good idea?

[cpitclaudel]

Yes, sounds great! We can add a link to the Alectryon header that pops up a little control window with various options, starting with this one. Do you want to look into doing that (I don't have much time atm)

[anton-trunov]

Awesome! I'll try to look into that.

[cpitclaudel]

Have you had time to look into this? I suspect it would be enough to add three rules in alectryon.css in the style of .alectryon-floating to disable the floating behavior.

[jjhugues]

Hi, I got the same issue and was curious to build a fix. I reviewed .alectryon-floating but could not convince myself how this part would influence hovering.

The following patch works for me: https://github.com/jjhugues/alectryon/commit/8075f7d7ea97348375097079aabb0450455ac481. It is probably not elegant or event correct though. Ctrl+h activates hovering. Reloading the page resets it. The idea is that the .js would add to the CSS the bit that activates the hovering. There might be a way to do the opposite.

Feel free to comment, I am by no mean a CSS/JS guru.

[cpitclaudel]

Sorry, the comment above was short and not super informative. Let me expand on the suggestion. We currently have three "styles" for goal display on hover: floating, windowed, and centered. The idea would be to add a new style no-hover; then add this rule:

.alectryon-no-hover .alectryon-sentence:hover .alectryon-output:not(:hover) {
    display: none;
}

(There's just one style needed, I was wrong to say 3.)

The advantage of this solution is that people who don't run JS still get the default hovering behavior, and it lines up with other options.

We'd then adjust the JS to make "no-hover" a selectable option, and update the CLI to make it easy to use that by default (see WEBPAGE_STYLE_CHOICES)

Alternatively, we can make the no-hover style a toggle, compatible with other display styles. In that case the simplest would be to condition all the :hover rules on an alectryon-hover class placed on the root of the document, and to toggle than on and off using js (defaulting to on).

[jjhugues]

Thanks for the clarification.

For the first design (i.e. a selectable option), you mean the list of styles would become floating, floating-no-hover, windowed, and centered. Is that correct? I can certainly propose something for this option.

For the second option, it means we need an additional keybinding to toggle similar to the hack I did. I am less familiar with CSS logic and would need more time to support this, if you want me to try

Now the question is: which option is preferable? I prefer 1. since I am not a fan of hovering. As long as we can set the default to no hovering for 2 through a configuration mechanism, 2. would be fine

[cpitclaudel]

For the first design (i.e. a selectable option), you mean the list of styles would become floating, floating-no-hover, windowed, and centered. Is that correct?

Yep. But windowed-no-hover and centered-no-hover would also make sense, hence option 2 "make the no-hover style a toggle".

Now the question is: which option is preferable? I prefer 1. since I am not a fan of hovering. As long as we can set the default to no hovering for 2 through a configuration mechanism, 2. would be fine

With option 2 we'd add a command line flag --no-hover, I'm guessing, so it would be easy to chose which behavior you want by default. Given that "no hover" is reasonable behavior for all current display styles, it feels orthogonal to the choice of style; hence I'm in favor of option 2.

I am less familiar with CSS logic

CSS is finicky. My intuition here is that the simplest thing to do is basically to prefix every rule that deals with hovering with a .alectryon-hover  class, which would be added or removed from the root element by a JS toggle.