//      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>