fix: move uri encoding to formatArgs

[jcreedcmu]

Resolves #109.

Moves the responsibility for calling fixedEncodeURIComponent to formatArgs. I tried to ensure that there's no double-encoding happening as a result of this change. I don't see any other callers of fixedEncodeURIComponent or encodeURIComponent after this change.

I locally tested that the behavior in #109 is eliminated. I tried copying and pasting well-formed code= and codez= URIs, editing, changing projects, Import-from-file functionality.

[Seasawher]

Is this change breaking?

[jcreedcmu]

I don't believe this violates any guarantee lean4web is making to the user or downstream code... But do correct me if I'm wrong in assuming the representation of the various jotai atoms used to hold url state is intended as "public api".

[Seasawher]

I run the following code for my online book. This may break?

function filePlay() {
  const playButtonIcon = document.querySelector("#lean-play-button");

  const playButtonLink = playButtonIcon.parentElement;

  playButtonLink.href = playButtonLink.href.replace(/\.md$/, ".lean");

  playButtonLink.href = playButtonLink.href.replace(
    "/booksrc/",
    "/LeanByExample/",
  );

  fetch(playButtonLink.href)
    .then((response) => response.text())
    .then((body) => {
      const escaped_code = encodeURIComponent(body);
      const url = `https://live.lean-lang.org/#code=${escaped_code}`;
      playButtonLink.href = url;
    });
}

filePlay();

[jcreedcmu]

I don't think it should break with this PR!

My intention and understanding of my code in this PR is that this use case would still work. The code that decodes the uri-encoded ${escaped_code} in links such as https://live.lean-lang.org/#code=${escaped_code} should be unaffected by this change.

The purpose of the PR is to ensure that when running instances of lean4web (such as https://live.lean-lang.org/) themselves produce URIs that are of the form #code=${escaped_code} (and this will naturally happen as you edit the code in the code editor if you have compression turned off in your settings) that the code in those URIs are always correctly uri-encoded. See the attached issue for an example of what can go wrong today.

But If you do think this PR will cause problems, I'm happy to hear more details!

[Seasawher]

Thank you!

[jcreedcmu]

You're welcome, and thanks for the clear example!

[joneugster]

Thank you for the fix!

[joneugster]

Is this change breaking?

Repeating what jcreedcmu said, this doesn't change the public API: any valid URL will still be valid.

It only fixes a clear bug in the link generation.