From 3769bb3811b1b8848cdf9bc7fa4ee1b7534bda00 Mon Sep 17 00:00:00 2001
From: Mark Kattenbelt <mark.kattenbelt@comlab.ox.ac.uk>
Date: Mon, 3 Nov 2008 15:00:30 +0000
Subject: [PATCH] centralise error when jumping

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@821 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/userinterface/model/GUITextModelEditor.java | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/prism/src/userinterface/model/GUITextModelEditor.java b/prism/src/userinterface/model/GUITextModelEditor.java
index da1cf699..12baa6bc 100644
--- a/prism/src/userinterface/model/GUITextModelEditor.java
+++ b/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)
 			{