Goto defintion for releases

This commit is contained in:
Kris De Volder
2017-07-19 15:33:02 -07:00
parent 9aa5ed36bb
commit 47dcb094c5
13 changed files with 317 additions and 60 deletions

View File

@@ -712,7 +712,7 @@ public class Editor {
}
/**
* Determines the position of (the middle of) a snippet of text in the document.
* Determines the position of a snippet of text in the document.
*
* @param contextSnippet A larger snippet containing the actual snippet to look for.
* This larger snippet is used to narrow the section of the document
@@ -725,6 +725,10 @@ public class Editor {
return r==null?null:r.getStart();
}
public Position positionOf(String snippet) throws Exception {
return positionOf(snippet, snippet);
}
/**
* Determines the range of a snippet of text in the document.
*
@@ -795,4 +799,5 @@ public class Editor {
this.selectionStart = this.selectionEnd = doc.toOffset(position);
}
}