tirix / mm-web-ui Goto Github PK

Currently, expanding is immediate, but collapsing takes time.
This is because each row has a different height, and the javascript animates the "max-height" property. A better solution might be to use the jQuery slideUp function.

As suggested by Norm in his google groups post:

The mouseover highlighting of steps affected by and affecting a step is very nice. Would it make sense to have it "stick" when the mouse moves off the proof (or off a specific column such as the Hyp column), so that the highlighting will persist when scrolling to a step off screen?

As suggested by Norm in his google group post:

add 4th and 5th highlight shades to indicate all steps that the current step depends on indirectly as well as all steps affected by the current step. Or instead, perhaps use the current shades to indicate indirect dependence instead of just direct dependence? I think indirect dependence is important for knowing that the current step didn't just pop out of the blue (esp. when its hypotheses are collapsed) but is a consequence of specific previous steps.

Was playing around with metamath and noticed again something
interesting. The structured view provides me with the ability to
click on symbols, and it leads me directly to their definition.

This seems not to work for the mapsto symbol. Why is this so?
For example here, I cannot click on mapsto:

sigaGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠})
http://metamath.tirix.org/df-sigagen.html

Means I cannot click on ↦ . The other symbols seem to work.
I wanted to explore what is behind the mapsto symbol.

Bug report migrated from news group:
https://groups.google.com/d/msg/metamath/Df4--aqbjwg/_TNTCDzoAgAJ

As suggested by FL:

The collapse/expand interface may be useful when you want to reduce the quantity
of displayed information. For instance if you have a theorem 1 and 3 premisses 5 7 9 you could
have only a table like

9 | ...   | a line of symbols
7 | ...   | a line of symbols
5 | ...   | a line of symbols
1 | 5 7 9 | a line of symbols

Easier to read.

Then if you want to know how to prove the step 9 you expand it and a page like

18 | ...     | a line of symbols
13 | ...     | a line of symbols
9  | 13 18   | a line of symbols

appears.

As suggested by David in his google group post:

If you have an "M" to emphasize indenting, there should be a way to undo it.

As suggested by Norm in his google groups post:

I understand the intent of alternating light mint green and lighter mint green in the full proof display - they make it easier to follow a line horizontally across the screen. For a collapsed display, I'm not sure if they are helpful since they no longer necessarily alternate. I found it slightly confusing at first to see so many different shades changing until I got used to it. I'm not sure if alternating shades really make that much of a difference for our purpose. They aren't used in ordinary text (that would be rather distracting), they are very helpful if not essential for tables with many columns and no cell borders, and proof displays are somewhere in between. I decided against it for the existing web pages because I felt the table cell borders already guide the eye sufficiently. In any case, you now have the line highlighted by a mouseover, so the purpose of alternating shades more or less disappears.

As proposed by Jan in his google groups post :

What confuses me: The exit/leave (also known as hoover) visual feedback of a proof line (it gets dark). Feels like in a disco.

As suggested by Jan in his google groups post:

You can check here: http://metamath.tirix.org/risefacval.html#6

Something is broken. There must be multiple event listeners on the same GUI event. When I click such a navigation at the same time the collapse/expand happens. You can try yourself in the above example, clicking first on 7 and then on 6 on the last line.

It will not show 6, since it thinks the click on 6 was a collapse. But the click on 6 is the same click as on 7, nothing todo with collapse/expand.

See also Jan's Gist entry.

As suggested by FL in his google groups post:

Simple. Use the arrow keys to move from one step to the other or open a step. It will be smoother.

You need an interface that is useful. With that kind of interface you will have to open or close
hundreds of steps while exploring the proof. Don't use the mouse, use the keyboard.

As suggested by David in his Google groups post:

Hypotheses and assertions should also have a "Metamath copy" button.

This is also missing in the pages for "syntax breakdown" axioms, like in df-chp.

Now I stepped into a new problem, that clicking on symbols doesn't
work. Now "Lim" doesn't work either. I wanted to click on "Lim" here:

𝜔 = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)
http://metamath.tirix.org/df-om.html

But no reaction of the system. I was expecting that it sends me to here:

(Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
http://metamath.tirix.org/df-lim.html

Also "Ord" doesn't work. On the other hand "On" and "U" do work.

Bug reported migrated from news group:
https://groups.google.com/d/msg/metamath/Df4--aqbjwg/ymQaqsAUBAAJ

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?

Also the links back to the non-structured unicode view don't work.
For example on this page:

http://metamath.tirix.org/df-lim.html

When clicking on the right top "Unicode version" in the structure
view I get the following error:

Not Found
The requested URL /mpeuni/df-lim.html was not found on this server.
http://metamath.tirix.org/mpeuni/df-lim.html

Bug reported migrated from news group:
https://groups.google.com/d/msg/metamath/Df4--aqbjwg/ymQaqsAUBAAJ