private synchronized void pushPlace(@NotNull Place place) {
    while (currentPos >= 0 && currentPos < history.size() - 1) {
      history.remove(history.size() - 1);
    }

    if (!history.isEmpty()) {
      final Place prev = history.get(history.size() - 1);
      if (prev.equals(place)) return;

      if (prev.isMoreGeneralFor(place)) {
        history.remove(prev);
      }
    }

    addPlace(place);
  }
private synchronized void pushPlace(@NotNull Place place)