}

var getAbsoluteBoundingRect = function(element) {
  const relative = element.getBoundingClientRect();
  return {
    left: relative.left + window.pageXOffset,
    right: relative.right + window.pageXOffset,
    top: relative.top + window.pageYOffset,
    bottom: relative.bottom + window.pageYOffset,
    height: relative.height,
    width: relative.width
  };
}

var drawArrow = function(index) {
  // This function is based on the great answer from SO:
  //   https://stackoverflow.com/a/39575674/11582326
  var start = document.querySelector("#start" + index);
  var end   = document.querySelector("#end" + index);
  var arrow = document.querySelector("#arrow" + index);

  var startRect = getAbsoluteBoundingRect(start);
  var endRect   = getAbsoluteBoundingRect(end);

  // It is an arrow from a token to itself, no need to visualize it.
  if (startRect.top == endRect.top &&
      startRect.left == endRect.left)
    return;

  // Each arrow is a very simple Bézier curve, with two nodes and
  // two handles.  So, we need to calculate four points in the window:
  //   * start node
  var posStart    = { x: 0, y: 0 };
  //   * end node
  var posEnd      = { x: 0, y: 0 };
  //   * handle for the start node
  var startHandle = { x: 0, y: 0 };
  //   * handle for the end node
  var endHandle   = { x: 0, y: 0 };
  // One can visualize it as follows:
  //
  //         start handle
  //        /
  //       X"""_.-""""X
  //         .'        \
  //        /           start node
  //       |
  //       |
  //       |      end node
  //        \    /
  //         `->X
  //        X-'
  //         \
  //          end handle
  //
  // NOTE: (0, 0) is the top left corner of the window.

  // We have 3 similar, but still different scenarios to cover:
  //
  //   1. Two tokens on different lines.
  //             -xxx
  //           /
  //           \
  //             -> xxx
  //      In this situation, we draw arrow on the left curving to the left.
  //   2. Two tokens on the same line, and the destination is on the right.
  //             ____
  //            /    \
  //           /      V
  //        xxx        xxx
  //      In this situation, we draw arrow above curving upwards.
  //   3. Two tokens on the same line, and the destination is on the left.
  //        xxx        xxx
  //           ^      /
  //            \____/
  //      In this situation, we draw arrow below curving downwards.
  const onDifferentLines = startRect.top <= endRect.top - 5 ||
    startRect.top >= endRect.top + 5;
  const leftToRight = startRect.left < endRect.left;

  // NOTE: various magic constants are chosen empirically for
  //       better positioning and look
  if (onDifferentLines) {
    // Case #1
    const topToBottom = startRect.top < endRect.top;
    posStart.x = startRect.left - 1;
    // We don't want to start it at the top left corner of the token,
    // it doesn't feel like this is where the arrow comes from.
    // For this reason, we start it in the middle of the left side
    // of the token.
    posStart.y = startRect.top + startRect.height / 2;

    // End node has arrow head and we give it a bit more space.
    posEnd.x = endRect.left - 4;
    posEnd.y = endRect.top;

    // Utility object with x and y offsets for handles.
    var curvature = {
      // We want bottom-to-top arrow to curve a bit more, so it doesn't
      // overlap much with top-to-bottom curves (much more frequent).
      x: topToBottom ? 15 : 25,
      y: Math.min((posEnd.y - posStart.y) / 3, 10)
    }

    // When destination is on the different line, we can make a
    // curvier arrow because we have space for it.
    // So, instead of using
    //
    //   startHandle.x = posStart.x - curvature.x
    //   endHandle.x   = posEnd.x - curvature.x
    //
    // We use the leftmost of these two values for both handles.
    startHandle.x = Math.min(posStart.x, posEnd.x) - curvature.x;
    endHandle.x = startHandle.x;

    // Curving downwards from the start node...
    startHandle.y = posStart.y + curvature.y;
    // ... and upwards from the end node.
    endHandle.y = posEnd.y - curvature.y;

  } else if (leftToRight) {
    // Case #2
    // Starting from the top right corner...
    posStart.x = startRect.right - 1;
    posStart.y = startRect.top;

    // ...and ending at the top left corner of the end token.
    posEnd.x = endRect.left + 1;
    posEnd.y = endRect.top - 1;

    // Utility object with x and y offsets for handles.
    var curvature = {
      x: Math.min((posEnd.x - posStart.x) / 3, 15),
      y: 5
    }

    // Curving to the right...
    startHandle.x = posStart.x + curvature.x;
    // ... and upwards from the start node.
    startHandle.y = posStart.y - curvature.y;

    // And to the left...
    endHandle.x = posEnd.x - curvature.x;
    // ... and upwards from the end node.
    endHandle.y = posEnd.y - curvature.y;

  } else {
    // Case #3
    // Starting from the bottom right corner...
    posStart.x = startRect.right;
    posStart.y = startRect.bottom;

    // ...and ending also at the bottom right corner, but of the end token.
    posEnd.x = endRect.right - 1;
    posEnd.y = endRect.bottom + 1;

    // Utility object with x and y offsets for handles.
    var curvature = {
      x: Math.min((posStart.x - posEnd.x) / 3, 15),
      y: 5
    }

    // Curving to the left...
    startHandle.x = posStart.x - curvature.x;
    // ... and downwards from the start node.
    startHandle.y = posStart.y + curvature.y;

    // And to the right...
    endHandle.x = posEnd.x + curvature.x;
    // ... and downwards from the end node.
    endHandle.y = posEnd.y + curvature.y;
  }

  // Put it all together into a path.
  // More information on the format:
  //   https://developer.mozilla.org/en-US/docs/Web/SVG/Tutorial/Paths
  var pathStr = "M" + posStart.x + "," + posStart.y + " " +
    "C" + startHandle.x + "," + startHandle.y + " " +
    endHandle.x + "," + endHandle.y + " " +
    posEnd.x + "," + posEnd.y;

  arrow.setAttribute("d", pathStr);
};

var drawArrows = function() {
  const numOfArrows = document.querySelectorAll("path[id^=arrow]").length;
  for (var i = 0; i < numOfArrows; ++i) {
    drawArrow(i);
  }
}

var toggleArrows = function(event) {
  const arrows = document.querySelector("#arrows");
  if (event.target.checked) {
    arrows.setAttribute("visibility", "visible");
  } else {
    arrows.setAttribute("visibility", "hidden");
  }
}

window.addEventListener("resize", drawArrows);
document.addEventListener("DOMContentLoaded", function() {
  // Whenever we show invocation, locations change, i.e. we
  // need to redraw arrows.
  document
    .querySelector('input[id="showinvocation"]')
    .addEventListener("click", drawArrows);
  // Hiding irrelevant lines also should cause arrow rerender.
  document
    .querySelector('input[name="showCounterexample"]')
    .addEventListener("change", drawArrows);
  document
    .querySelector('input[name="showArrows"]')
    .addEventListener("change", toggleArrows);
  drawArrows();
  // Default highlighting for the last event.
  highlightArrowsForSelectedEvent();
});
</script>