Break Definition cycles in hovers

[kohlhase]

When we have a definition that introduces multiple definienda, then hovering on the term references of the others gives the same definition that you are already looking at.

This is a source of confustion to students (they reported). In this case we should have a hover that says something like "You are already looking at the right definition. Foo is defined here."

[Jazzpirate]

There are multiple possible solutions.

1. don't use \sn/\sr, use \definame/\definiendum in the sources.
2. Disable the popups in the frontend/viewer for \sn/\sr of definienda-that-are-not-marked-as-definienda in definitions entirely (or replace them by some other functionality, see below), or have then frontend/viewer auto-mark them as definienda. Somewhat annoying to implement, since which terms exactly are even definienda may only be known retroactively, since which terms are definienda is also inferred from the usage of \definame/\definiendum. Ideally, sTeX would just automatically mark term references as definienda, but then we would have to add every definiendum to the for=-list of the definition (since tex can't "look back").
3. Have the backend return some default for \sn/\sr of definienda-that-are-not-marked-as-definienda in definitions. That would entail encoding a lot more information in the backend-requests, because of course the backend doesn't know (necessarily) where a hover occurs - and arguably it shouldn't have to.

I think 3. is the worst option. 2. is annoying but feasible. 1. is straight-forward and to some extent the semantically most adequate (why use \sn/\sr at all if you don't want the only real functionality that \sn/\sr give you?), but also slightly overheady for semantic macros (i.e. all definienda-semantic macros would need to be wrapped in a \defnotation).

In general, I would not recommend having hovers at all that just say something equivalent to "no hover for you!" - I think from a UX perspective that is both nonsensical and confusing: A popup naturally grabs attention, so whatever it shows should be actually informative. Nobody complained that they're confused that (actually marked-as-such) definienda don't show hovers, so just having no popups seems most adequate to me.

If we want them to do something informative, we may want to have them do something else on hover - e.g. we could highlight the definiens (with a yellow background maybe?) right in the document (if existent) instead of having a popup...

[kohlhase]

I am not sure that you understand the problem. I have added a screenshot above to make it clearer. The problem is that in the hover there is a (legitimate) term reference that (legitimately) points to (a definiendum in) the definition it in. That leads into a popup cycle the students are confused by. That is the only thing I am complaining about, and nothing your reply can fix (if as I claim the markup is legitimate).

[Jazzpirate]

Yes, the problem is that there are term references to terms that are being defined in the very same definition. i.e., they are definienda, not just term references. The markup is either not legitimate, or we need a special treatment for "term references in definitions in which they are definienda", which, I would argue, is the exact same treatment as for explicitly-marked-as definienda except for maybe the color :D

[kohlhase]

I am a bit surprised that we would disagree on something soooo fundamental as what is a definiendum and what is a term reference, but I think you are wrong. I suspect that the root cause of this might be that I consider word occurrences in a text to carry the property of being a definiendum or a definiens. And so one occurrence of a word (or glyph) can be a definiendum and another of the same word a reference to the first. And I think that this is at work here. I think we agree what we should do something here to remedy the confusing situation.

[Jazzpirate]

By "definiendum", I just mean "the term being defined". And then there are term occurrences that are explicitly marked as \definiendum. So maybe let's distinguish between "definiendum" and \definiendum :D But either way, that's just terminology. The point is, there are "definienda" that are not \definiendums. I'm not entirely convinced that they should not be \definiendums then, but I'm also not convinced that they should be.

But my intuition is: We turned off popups for \definiendums, because they're redundant. Now the only functionality they have is "being magenta". We can do the same for the "definienda" that are not \definiendums (although that's not going to be trivial, because identifying them is a pain - and in pdf it's impossible, because tex can't do it at all), where the only functionality then is "being turqoise-ish".

What's annoying about that is that they then look like any other term reference, so I agree that there's the induced expectation that one should see a popup on hover. But if we give them a popup that explains why there's no popup, I'm almost certain we're doing something wrong from a UX POV ;)

[kohlhase]

OK, so we are in agreement, only that I feel very uncomfortable with the name "Definiendum" for "term references that happen to be in a definition for themselves". Maybe we can call them "locally defined terms" and keep the name Definiendum for what you call \definiendums?

Currently, locally defined terms are blue and carry a hover, and Definienda (in mynarrow sense) are magenta. I would like to keep the colors, but drop the hover on the locally defined terms.

Is this something we can agree on?

[Jazzpirate]

The dictionary disagrees with your terminology :D but yes, and now there are three ways in principle to drop the hovers, see my first comment modulo terminology :)