tirix / mm-web-ui Goto Github PK
View Code? Open in Web Editor NEWA user interface for the Metamath web pages
License: MIT License
A user interface for the Metamath web pages
License: MIT License
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 π΄
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
π Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. πππ
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google β€οΈ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.