visitExtensibleArrow method

@override String visitExtensibleArrow(ExtensibleArrowNode node)

Implementation

@override
String visitExtensibleArrow(ExtensibleArrowNode node) {
  final arrowChar = switch (node.direction) {
    ArrowDirection.right => "→",
    ArrowDirection.left => "←",
    ArrowDirection.both => "↔",
    ArrowDirection.hookRight => "↪",
    ArrowDirection.hookLeft => "↩",
    ArrowDirection.rightDouble => "⇒",
    ArrowDirection.leftDouble => "⇐",
    ArrowDirection.bothDouble => "⇔",
    ArrowDirection.mapsto => "↦",
    ArrowDirection.equal => "=",
  };

  final arrow = '<mo stretchy="true">$arrowChar</mo>';
  final above = visit(node.content);
  final below = node.below != null ? visit(node.below!) : null;

  if (below != null) {
    return "<munderover>$arrow${_mrow(below)}${_mrow(above)}</munderover>";
  } else {
    return "<mover>$arrow${_mrow(above)}</mover>";
  }
}