From 61eb14f65e73a9b3d0ea6eca6b04da804a4ff61b Mon Sep 17 00:00:00 2001
From: jeff
Date: Sun, 8 Mar 2015 13:49:44 -0400
Subject: lots of small tweaks and improvements

---
 src/cuchaz/enigma/gui/GuiTricks.java | 58 ++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)

(limited to 'src/cuchaz/enigma/gui/GuiTricks.java')

diff --git a/src/cuchaz/enigma/gui/GuiTricks.java b/src/cuchaz/enigma/gui/GuiTricks.java
index df9e221..5a3a01d 100644
--- a/src/cuchaz/enigma/gui/GuiTricks.java
+++ b/src/cuchaz/enigma/gui/GuiTricks.java
@@ -11,11 +11,21 @@
 package cuchaz.enigma.gui;
 
 import java.awt.Font;
+import java.awt.Rectangle;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
 import java.awt.event.MouseEvent;
 
 import javax.swing.JComponent;
+import javax.swing.JEditorPane;
 import javax.swing.JLabel;
+import javax.swing.SwingUtilities;
+import javax.swing.Timer;
 import javax.swing.ToolTipManager;
+import javax.swing.text.BadLocationException;
+import javax.swing.text.Highlighter.HighlightPainter;
+
+import cuchaz.enigma.analysis.Token;
 
 public class GuiTricks {
 	
@@ -33,4 +43,52 @@ public class GuiTricks {
 		manager.mouseMoved(new MouseEvent(component, MouseEvent.MOUSE_MOVED, System.currentTimeMillis(), 0, 0, 0, 0, false));
 		manager.setInitialDelay(oldDelay);
 	}
+	
+	public static void navigateToToken(final JEditorPane editor, final Token token, final HighlightPainter highlightPainter) {
+		
+		// set the caret position to the token
+		editor.setCaretPosition(token.start);
+		editor.grabFocus();
+		
+		try {
+			// make sure the token is visible in the scroll window
+			Rectangle start = editor.modelToView(token.start);
+			Rectangle end = editor.modelToView(token.end);
+			final Rectangle show = start.union(end);
+			show.grow(start.width * 10, start.height * 6);
+			SwingUtilities.invokeLater(new Runnable() {
+				@Override
+				public void run() {
+					editor.scrollRectToVisible(show);
+				}
+			});
+		} catch (BadLocationException ex) {
+			throw new Error(ex);
+		}
+		
+		// highlight the token momentarily
+		final Timer timer = new Timer(200, new ActionListener() {
+			private int m_counter = 0;
+			private Object m_highlight = null;
+			
+			@Override
+			public void actionPerformed(ActionEvent event) {
+				if (m_counter % 2 == 0) {
+					try {
+						m_highlight = editor.getHighlighter().addHighlight(token.start, token.end, highlightPainter);
+					} catch (BadLocationException ex) {
+						// don't care
+					}
+				} else if (m_highlight != null) {
+					editor.getHighlighter().removeHighlight(m_highlight);
+				}
+				
+				if (m_counter++ > 6) {
+					Timer timer = (Timer)event.getSource();
+					timer.stop();
+				}
+			}
+		});
+		timer.start();
+	}
 }
-- 
cgit v1.2.3