Browse Source

centralise error when jumping

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@821 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Mark Kattenbelt 17 years ago
parent
commit
3769bb3811
  1. 9
      prism/src/userinterface/model/GUITextModelEditor.java

9
prism/src/userinterface/model/GUITextModelEditor.java

@ -682,7 +682,14 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen
{
try
{
editor.setCaretPosition(computeDocumentOffset(parseError.getBeginLine(), parseError.getBeginColumn()));
int offset = computeDocumentOffset(parseError.getBeginLine(), parseError.getBeginColumn());
// scroll to center as much as possible.
editor.setCaretPosition(offset);
Rectangle r1 = editor.modelToView(offset);
int dy = (editor.getVisibleRect().height - r1.height) / 2;
Rectangle r2 = new Rectangle(0, r1.y - dy,editor.getVisibleRect().width, r1.height + 2*dy);
editor.scrollRectToVisible(r2);
}
catch (BadLocationException e)
{

Loading…
Cancel
Save