@Nullable
  private synchronized List<RangeHighlighter> getOrCreateHighlighters(boolean init) {
    var editor = myEditor;
    if (editor == null || editor.isDisposed()) return null;
    var highlighters = editor.getUserData(COVERAGE_HIGHLIGHTERS);
    if (highlighters == null && init) {
      highlighters = new ArrayList<>();
      editor.putUserData(COVERAGE_HIGHLIGHTERS, highlighters);
    }
    return highlighters;
  }
@Nullable
  private synchronized List<RangeHighlighter> getOrCreateHighlighters(boolean init)