search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

How do I close pop-up window when navigating document with Ctrl-Down/Up? #23

Closed anton-trunov closed 3 years ago

anton-trunov commented 3 years ago

When I navigate a document with Ctrl(Cmd)-Down, Alectryon reveals Coq's response but it seems to be impossible to simply close the pop-up window with Coq's response without pressing Ctrl-Down (or Ctrl-Up). Sometimes I just want to have the current line highlighted in bold but no pop-up.

Clicking bubbles does not help in this case because bubbles do not get activated during navigation.

cpitclaudel commented 3 years ago

🤔 you can press Ctrl+click on the bolded line to remove the pop up, but that also removes the highlight. Do you want just a highlight with no proof display?

anton-trunov commented 3 years ago

you can press Ctrl+click on the bolded line to remove the pop up

Actually, the pop-up stays if I click the bolded line (tested in Chrome and Safari).

Do you want just a highlight with no proof display?

Yes, exactly that. I'd like to have it as a context anchor while I talk about surrounding code / text.

cpitclaudel commented 3 years ago

Actually, the pop-up stays if I click the bolded line (tested in Chrome and Safari).

Even after you move the mouse away? It stays because you're still hovering, until you move your mouse (but only if the line has been unbolded)

Yes, exactly that. I'd like to have it as a context anchor while I talk about surrounding code / text.

Ah, very interesting use case; the code doesn't do that at the moment. I think the easiest would be to write a bit of extra code for it; do you need help?

anton-trunov commented 3 years ago

Yep, the pop-up still stays on even if I move the mouse cursor away. If I click the bolded line then the bubble toggles active/inactive but the pop-up still does not go away.

I think the easiest would be to write a bit of extra code for it; do you need help?

I was thinking the navigating code should make the bubble active for the bolded line, then clicking on the line would make pop-ups disapper. Does it sound about right?

anton-trunov commented 3 years ago

I think I did something wrong initially. If I click on the bolded line that makes it non-bold and after I move the cursor away the pop-up indeed disappears.

cpitclaudel commented 3 years ago

Closing this issue based on the latest comment, but let me know if I misunderstood. (Also, if some of your materials are public, I'd love to link to them from the README :) !)

anton-trunov commented 3 years ago

Also, if some of your materials are public, I'd love to link to them from the README

Here you go https://github.com/anton-trunov/csclub-coq-course-spring-2021. Thanks for your interest!