[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] A symbol reference system works on the HTML-ized MML
Dear Mizar Users,
I would like to inform you of a developing symbol reference system.
You can access the website at the following address:
http://webmizar.cs.shinshu-u.ac.jp/mmlfe/current/
I would be really happy if you could give me some advice, new ideas,
bug reports or enhancement requests about that,
I also wish you could inform me of the update information of the main
HTML-ized MML site (http://mizar.org/version/current/html/) so that
I'll recreate the reference system as soon as possible. (It will take
a few hours from Japan.)
** Summary **
The program parses HTML-ized MML files from website
(http://mizar.org/version/current/html/) and generates HTML files. It
is similar to documentation generator like Doxygen.
URL: http://webmizar.cs.shinshu-u.ac.jp/mmlfe/current/
Source code: https://github.com/aabaa/mmlfrontend (written in Python)
** Features **
[Left pain]
- Symbol List
All symbols defined in MML (predicate, structure, mode, functor,
attribute) are in a list in the left pain. By clicking a symbol, you
can jump to its page.
- Incremental Search
You can narrow the symbol list by inputting words in the upper-left
search-box. If several words (separated with spaces) are input, the
system squeezes the list into symbols which includes all the input
words. The search logic is case-insensitive
[Right pain]
- Source Code
The HTML structure of source code are copied from Mizar/MML Wiki. By
clicking a keyword, you can jump to the definition.
- Referrers List
You can check symbols referencing to a focusing symbol.
Sincerely,
Kazuhisa Nakasho
--
NAKASHO Kazuhisa (Shinshu University, Japan)
e-mail : k.nakasho@gmail.com, 13st205f@shinshu-u.ac.jp