Method jumpTo

src/ide.ts:1043–1052

(id:string)

  }, 0);

  jumpTo(id:string) {
    for(let span of this.getAllSpans()) {
      if(span.source.id === id) {
        let loc = span.find();
        if(!loc) break;
        this.cm.scrollIntoView(loc, 20);
        break;
      }
    }
  }

  scrollToPosition(position:Position) {
    let top = this.cm.cursorCoords(position, "local").top;