tooltips
Josef Urban <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAFP4q17wDS6kHOpJpL_OT7zmbbYbQ3mWi4=Bq6pbhzkFuSHteA@mail.gmail.com> |
Hi, the HTML/ATP services now use tooltips (balloon help as in Emacs) for showing thesis, the meaning of the used library references, the meaning of property/correctness formulas, proofs, and ATP explanations. Clicking should work as before (it seems good to combine both these methods when reading proofs). A normal example is http://mizar.cs.ualberta.ca/~mptp/7.13.01_4.181.1147/html/card_1.html . An example with tooltips over the "by/from" keywords showing also ATP explanations is http://mizar.cs.ualberta.ca/~mptp/cgi-bin/MizAR.cgi?ProblemSource=URL&FormulaURL=http://mizar.cs.ualberta.ca/~mptp/mml4.181.1147/mml/card_1.miz&MMLVersion=4.181.1147&Name=Tst1&GenATP=1&HTMLize=1 (or use the interface at http://mizar.cs.ualberta.ca/~mptp/MizAR.html, or the html-ization from Emacs). I have only tested with Firefox and Chrome so far, no idea what the code does in Explorer. Best, Josef