search

tirix / mm-web-ui

A user interface for the Metamath web pages
MIT License
4 stars 0 forks source link

Make formulas clickable to give access to symbol definitions #6

Closed tirix closed 6 years ago

tirix commented 6 years ago

As mentioned by Jan in his google groups post:

What I didn't find: Cross referencing. I looked at http://metamath.tirix.org/risefacval.html, and wanted spontaneously click on RiseFac already in the theorem statement, to see its definition or get more info about it.

But the relationship between symbols and theorems is a difficult one I guess. In the present case I found usage of df-risefac itself in the following proof, which gave me the information I was looking for to roughly understand what the proof is about. The other symbol, prod, was a little bit more difficult.

Also I dont know whether there is really a systematic to find something like a definition of a symbol. Do all symbols have an explicit definition in the system, or are some symbols introduced otherwise. Anyway it seems that my inner childs rather wants to click on symbols directly in the theorem. The the other new feratures. Clickable symbols need not be underlined, so the links need to disturb the new and pretty rendering, this can be configured by CSS style sheets...

But I guess it will blow up the output and the traffic for a web site. Maybe something intelligent can be done, that only the first occurence of a symbol gets a link?

jkingdon commented 6 years ago

The definitions are at the bottom of the page - "df-risefac 25244" in this case. Making the first occurrence clickable might make this more findable. I guess we'd have to see whether people would understand that, or whether they'd click there wanting something else.

digama0 commented 6 years ago

I don't think "first use" is a very reliable measure. The first place a user sees a notation is probably not the first use on the page, particularly since metamath proofs are best read backwards, and it is annoying to scour the page looking for the first occurrence. The syntax hints provide a unified location to put this information, but if you want to click on symbols in the formula directly then I would suggest just linking all symbols. Not sure how to set MathJax up for that though.

tirix commented 6 years ago

From an implementation point of view, it is surely more practical to link all symbols. Setting an "href" attribute in MathML seems to work. As an experiment, I've added links for all the "log" tokens in ~birthday. The default behavior does not seem to change the mouse pointer when hovering over them, and I would rather change back the color to the original black for constants, but this can be easily changed in CSS. I've added this manually in the rule for 'log'. It might be necessary to create the same kind of link for all Would it be sufficient to add the links only to constants?

tirix commented 6 years ago

The difficulty here will be to provide links for constructs which do not have an actual token, like complex division, complex conjugate or the binomial coefficient : there is nothing to click on. In those cases, I'm not sure it makes sense to add the links to the fractional horizontal bar, or to the parenthesis (and I'm not sure I could do it). We would probably have to skip those cases.

tirix commented 6 years ago

PS. In the mean time, I've added more links to ~birthday.

tirix commented 6 years ago

Links are colored correctly since commit 65f5d49.

The actual links are coming from the STS definition rule file. For set.mm, this is set-mathml.mmts, tracked in the set.mm project. Most links are available since set.mm commits b33b5b5, 6ceae47 and 2113462.