Formalmath.org

The new HTML rendering of IsarMathLib is ready.

Creating it was easier than I had expected. The most tricky part of the Isar to HTML translator is the Isar parser, but that was done when creating the TiddlyWiki rendering, and didn’t require any changes. Producing HTML from internal representation was just a simple rewrite of the existing TiddlyWiki markup generator. I had to learn some JavaScript and haXe to implement expanding proofs and reference hints, but not much and it was an interesting experience.The CSS layout was created with an online frameset generator with some minor tweaks.

There is one remaining serious issue that I don’t know how to resolve. Some proofs don’t expand on click. One can see an example of this problem in the proof of lemma func1_1_L12 in the func1 theory. The only subproof there does not change cursor and background color on mouse hover (implemented with CSS) and does not expand on click (haXe and JavaScript). Curiously, TiddlyWiki presentation has a very similar problem, see the proof of prod_list_of_lists in the Semigroup_ZF tiddler. This happens in Firefox 3.0.5 on Ubuntu and IE7 and Firefox on Windows XP. If you have an idea what might be causing this, please let me know.

P.S. This turned out to be a jsMath issue.

Advertisements

Tags: , , , ,

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


%d bloggers like this: