Online tutorial's links do not support Cmd-click, do not preserve browser history, and more

[carlpaten-ivadolabs]

I'm listing several bugs here, but they all have the same root cause and fix, related to how internal links are handled.

Bug 1: from https://leanprover.github.io/tutorial/index.html, I click the drop-down list and select "02 Dependent Type Theory". The URL address does not meaningfully change; if I send the address to someone and they open it, it brings them to chapter 1.

Expected behaviour: if I am on the chapter 2 page, the URL should be a permalink to chapter 2.

Bug 2: if I go further down this page, there is a link to the chapter on type classes. Cmd-click (OS X) creates a new tab with the chapter in question, but the current page also moves to the type classes chapter.

Expected behaviour: Cmd-click should have the same effect as right-click -> open in new tab.

Note: this is probably reproducible on Windows with Ctrl-click.

Bug 3: after opening one internal link, all other internal links appear purple, as if visited.

Expected behaviour: only links to chapters which I've actually visited should appear purple.

[carlpaten-ivadolabs]

I'll take this occasion to express how excited I am about Lean. The tutorial is especially user-friendly.

[soonhokong]

Thanks for reporting the bugs! I'll fix them soon.

[carlpaten-ivadolabs]

You're welcome. Normally I'd try to contribute pull requests, but finals are looming in Canada so I can't start anything. Good luck.

[soonhokong]

@LilRed, sure. When you have a chance, please contribute to this repo :-) Good luck with your finals!

[carlpaten-ivadolabs]

There's a related issue which I'm not sure how to consistently reproduce. Sometimes, when using the drop-down list to go to one chapter to the next, I end up on, say, section 4.3 instead of the top of the Chapter 4 page. I'm going to open an issue once I figure out how to repro.