highlightDef()

in src/overlay/gather-markers.ts [247:275]


  highlightDef(editorDef: EditorDef) {
    let editor = editorDef.editor;
    let def = editorDef.def;
    let doc = editor.getDoc();

    // Add marker for the definition symbol.
    let marker = doc.markText(
      { line: def.location.first_line - 1, ch: def.location.first_column },
      { line: def.location.last_line - 1, ch: def.location.last_column },
      { className: DEFINITION_CLASS }
    );
    let defSelection = new DefSelection({
      editorDef: editorDef,
      cell: editorDef.cell
    });
    let clickHandler = (_: py.Cell, __: py.Location, selected: boolean, event: MouseEvent) => {
      if (selected) {
        if (!event.shiftKey) {
          this._model.deselectAll();
        }
        this._model.selectDef(defSelection);
      } else {
        this._model.deselectDef(defSelection);
      }
    };
    this._defMarkers.push(
      new DefMarker(marker, editor, def, def.location, def.node, editorDef.cell, clickHandler)
    );
  }