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 : [email protected], [email protected]