// redirect rules for URL fragments (client-side) to prevent link rot.
// this must be done on the client side, as web servers do not see the fragment part of the URL.
// it will only work with JavaScript enabled in the browser, but this is the best we can do here.
// see source/_redirects for path redirects (server-side)

// redirects are declared as follows:
// each entry has as its key a path matching the requested URL path, relative to the mdBook document root.
//
//     IMPORTANT: it must specify the full path with file name and suffix
//
// each entry is itself a set of key-value pairs, where
// - keys are anchors on the matched path.
// - values are redirection targets relative to the current path.

const redirects = @REDIRECTS_JSON@;

// the following code matches the current page's URL against the set of redirects.
//
// it is written to minimize the latency between page load and redirect.
// therefore we avoid function calls, copying data, and unnecessary loops.
// IMPORTANT: we use stateful array operations and their order matters!
//
// matching URLs is more involved than it should be:
//
// 1. `document.location.pathname` can have an arbitrary prefix.
//
// 2. `path_to_root` is set by mdBook. it consists only of `../`s and
//    determines the depth of `<path>` relative to the prefix:
//
//          `document.location.pathname`
//        |------------------------------|
//        /<prefix>/<path>/[<file>[.html]][#<anchor>]
//                  |----|
//              `path_to_root` has same number of path segments
//
//    source: https://phaiax.github.io/mdBook/format/theme/index-hbs.html#data
//
// 3. the following paths are equivalent:
//
//        /foo/bar/
//        /foo/bar/index.html
//        /foo/bar/index
//
//  4. the following paths are also equivalent:
//
//        /foo/bar/baz
//        /foo/bar/baz.html
//

let segments = document.location.pathname.split('/');

let file = segments.pop();

// normalize file name
if (file === '') { file = "index.html"; }
else if (!file.endsWith('.html')) { file = file + '.html'; }

segments.push(file);

// use `path_to_root` to discern prefix from path.
const depth = path_to_root.split('/').length;

// remove segments containing prefix. the following works because
// 1. the original `document.location.pathname` is absolute,
//    hence first element of `segments` is always empty.
// 2. last element of splitting `path_to_root` is also always empty.
// 3. last element of `segments` is the file name.
//
// visual example:
//
//     '/foo/bar/baz.html'.split('/') -> [ '', 'foo', 'bar', 'baz.html' ]
//          '../'.split('/')          -> [ '..', '' ]
//
// the following operations will then result in
//
//     path = 'bar/baz.html'
//
segments.splice(0, segments.length - depth);
const path = segments.join('/');

// anchor starts with the hash character (`#`),
// but our redirect declarations don't, so we strip it.
// example:
//     document.location.hash -> '#foo'
//     document.location.hash.substring(1) -> 'foo'
const anchor = document.location.hash.substring(1);

const redirect = redirects[path];
if (redirect) {
  const target = redirect[anchor];
  if (target) {
    document.location.href = target;
  }
}