1 files changed, 58 insertions, 0 deletions

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();
+        }
 }