Re: [mizar] Some bugs (or features)

[Josef Urban <josef.urban@gmail.com>]

Dear Boris,

On Mon, Sep 12, 2011 at 9:37 AM, Boris Schminke <schminkeba@gmail.com> wrote:
> Dear All,
> I've found some strange things. The first one happens when one try to
> download HTML-linked articles from ftp://mizar.uwb.edu.pl/pub/xmlmml/
> and browse them with Chromium or Google Chrome locally (both under
> Linux and Windows). Proofs won't expand then with the error
> ""XMLHttpRequest cannot load file:///... Cross origin requests are
> only supported for HTTP."  The issue and workarounds are discussed
> here: http://code.google.com/p/chromium/issues/detail?id=40787
> According to this discussion I think that there is nothing to be done
> at Mizar's side. Users can either use --allow-file-access-from-files
> option while running Chromium locally or use Firefox/IE/Safari.

Yes, I understand the security concerns, but I was not exactly happy
when Firefox 3 introduced this. I guess if there are people still
using the HTML locally, we could produce a version that does not use
AJAX for fetching the proofs dynamically, and instead contains them
all directly in the HTML files. The size (and loading times on slower
computers) of such files will obviously increase.

A bit more involved solution that I have worked on recently is to use
the remote server-based HTML-ization from Emacs, which links the
articles to the HTML-ized library at the server. This is also much
faster than browser-based XSLT processing (which also broke with
Firefox 3 I think). The downside is that internet connection is
needed.


Btw., Czeslaw Bylinski has fixed the recent bug in lisppars that
resulted in broken skeletonization in Emacs. The fix should be
available in the next MML release (1133).

Best,
Josef



> The second one is a typo in MEASURE2 article
> (http://mizar.org/version/current/html/measure2.html). In the title
> there is a mentioning of discrete categories but there are none of
> them in the article and the title at the FM page. I think that this
> mentioning should be deleted.
>
> --
> Yours,
> Boris.
>