View


1   /*
2    * View.java - jEdit view
3    * :tabSize=8:indentSize=8:noTabs=false:
4    * :folding=explicit:collapseFolds=1:
5    *
6    * Copyright (C) 1998, 2004 Slava Pestov
7    *
8    * This program is free software; you can redistribute it and/or
9    * modify it under the terms of the GNU General Public License
10   * as published by the Free Software Foundation; either version 2
11   * of the License, or any later version.
12   *
13   * This program is distributed in the hope that it will be useful,
14   * but WITHOUT ANY WARRANTY; without even the implied warranty of
15   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
16   * GNU General Public License for more details.
17   *
18   * You should have received a copy of the GNU General Public License
19   * along with this program; if not, write to the Free Software
20   * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
21   */
22  
23  package org.gjt.sp.jedit;
24  
25  //{{{ Imports
26  import javax.swing.event.*;
27  import javax.swing.*;
28  import java.awt.*;
29  import java.awt.event.*;
30  import java.io.IOException  ;
31  import java.io.StreamTokenizer  ;
32  import java.io.StringReader  ;
33  import java.net.Socket  ;
34  import java.util.*;
35  import java.util.List  ;
36  
37  import org.gjt.sp.jedit.msg.*;
38  import org.gjt.sp.jedit.gui.*;
39  import org.gjt.sp.jedit.search.*;
40  import org.gjt.sp.jedit.textarea.*;
41  import org.gjt.sp.jedit.textarea.TextArea;
42  import org.gjt.sp.jedit.input.InputHandlerProvider;
43  //}}}
44  
45  /**
46   * A <code>View</code> is jEdit's top-level frame window.<p>
47   *
48   * In a BeanShell script, you can obtain the current view instance from the
49   * <code>view</code> variable.<p>
50   *
51   * The largest component it contains is an {@link EditPane} that in turn
52   * contains a {@link org.gjt.sp.jedit.textarea.JEditTextArea} that displays a
53   * {@link Buffer}.
54   * A view can have more than one edit pane in a split window configuration.
55   * A view also contains a menu bar, an optional toolbar and other window
56   * decorations, as well as docked windows.<p>
57   *
58   * The <b>View</b> class performs two important operations
59   * dealing with plugins: creating plugin menu items, and managing dockable
60   * windows.
61   *
62   * <ul>
63   * <li>When a view is being created, its initialization routine
64   * iterates through the collection of loaded plugins and constructs the
65   * <b>Plugins</b> menu using the properties as specified in the
66   * {@link EditPlugin} class.</li>
67   * <li>The view also creates and initializes a
68   * {@link org.gjt.sp.jedit.gui.DockableWindowManager}
69   * object.  This object is
70   * responsible for creating, closing and managing dockable windows.</li>
71   * </ul>
72   *
73   * This class does not have a public constructor.
74   * Views can be opened and closed using methods in the <code>jEdit</code>
75   * class.
76   *
77   * @see org.gjt.sp.jedit.jEdit#newView(View)
78   * @see org.gjt.sp.jedit.jEdit#newView(View,Buffer)
79   * @see org.gjt.sp.jedit.jEdit#newView(View,Buffer,boolean)
80   * @see org.gjt.sp.jedit.jEdit#closeView(View)
81   *
82   * @author Slava Pestov
83   * @author John Gellene (API documentation)
84   * @version $Id: View.java 8676 2007-01-19 20:14:58Z kpouer $
85   */
86  public class View extends JFrame implements EBComponent, InputHandlerProvider
87  {
88      //{{{ User interface
89  
90      //{{{ ToolBar-related constants
91  
92      //{{{ Groups
93      /**
94       * The group of tool bars above the DockableWindowManager
95       * @see #addToolBar(int,int,java.awt.Component)
96       * @since jEdit 4.0pre7
97       */
98      public static final int TOP_GROUP = 0;
99  
100     /**
101      * The group of tool bars below the DockableWindowManager
102      * @see #addToolBar(int,int,java.awt.Component)
103      * @since jEdit 4.0pre7
104      */
105     public static final int BOTTOM_GROUP = 1;
106     public static final int DEFAULT_GROUP = TOP_GROUP;
107     //}}}
108 
109     //{{{ Layers
110 
111     // Common layers
112     /**
113      * The highest possible layer.
114      * @see #addToolBar(int,int,java.awt.Component)
115      * @since jEdit 4.0pre7
116      */
117     public static final int TOP_LAYER = Integer.MAX_VALUE;
118 
119     /**
120      * The default layer for tool bars with no preference.
121      * @see #addToolBar(int,int,java.awt.Component)
122      * @since jEdit 4.0pre7
123      */
124     public static final int DEFAULT_LAYER = 0;
125 
126     /**
127      * The lowest possible layer.
128      * @see #addToolBar(int,int,java.awt.Component)
129      * @since jEdit 4.0pre7
130      */
131     public static final int BOTTOM_LAYER = Integer.MIN_VALUE;
132 
133     // Layers for top group
134     /**
135      * Above system tool bar layer.
136      * @see #addToolBar(int,int,java.awt.Component)
137      * @since jEdit 4.0pre7
138      */
139     public static final int ABOVE_SYSTEM_BAR_LAYER = 150;
140 
141     /**
142      * System tool bar layer.
143      * jEdit uses this for the main tool bar.
144      * @see #addToolBar(int,int,java.awt.Component)
145      * @since jEdit 4.0pre7
146      */
147     public static final int SYSTEM_BAR_LAYER = 100;
148 
149     /**
150      * Below system tool bar layer.
151      * @see #addToolBar(int,int,java.awt.Component)
152      * @since jEdit 4.0pre7
153      */
154     public static final int BELOW_SYSTEM_BAR_LAYER = 75;
155 
156     /**
157      * Search bar layer.
158      * @see #addToolBar(int,int,java.awt.Component)
159      * @since jEdit 4.0pre7
160      */
161     public static final int SEARCH_BAR_LAYER = 75;
162 
163     /**
164      * Below search bar layer.
165      * @see #addToolBar(int,int,java.awt.Component)
166      * @since jEdit 4.0pre7
167      */
168     public static final int BELOW_SEARCH_BAR_LAYER = 50;
169 
170     // Layers for bottom group
171     /**
172      * @deprecated Status bar no longer added as a tool bar.
173      */
174     public static final int ABOVE_ACTION_BAR_LAYER = -50;
175 
176     /**
177      * Action bar layer.
178      * @see #addToolBar(int,int,java.awt.Component)
179      * @since jEdit 4.2pre1
180      */
181     public static final int ACTION_BAR_LAYER = -75;
182 
183     /**
184      * Status bar layer.
185      * @see #addToolBar(int,int,java.awt.Component)
186      * @since jEdit 4.2pre1
187      */
188     public static final int STATUS_BAR_LAYER = -100;
189 
190     /**
191      * Status bar layer.
192      * @see #addToolBar(int,int,java.awt.Component)
193      * @since jEdit 4.2pre1
194      */
195     public static final int BELOW_STATUS_BAR_LAYER = -150;
196     //}}}
197 
198     //}}}
199 
200     //{{{ getDockableWindowManager() method
201     /**
202      * Returns the dockable window manager associated with this view.
203      * @since jEdit 2.6pre3
204      */
205     public DockableWindowManager getDockableWindowManager()
206     {
207         return dockableWindowManager;
208     } //}}}
209 
210     //{{{ getToolBar() method
211     /**
212      * Returns the view's tool bar.
213      * @since jEdit 4.2pre1
214      */
215     public Box getToolBar()
216     {
217         return toolBar;
218     } //}}}
219 
220     //{{{ addToolBar() method
221     /**
222      * Adds a tool bar to this view.
223      * @param toolBar The tool bar
224      */
225     public void addToolBar(Component toolBar)
226     {
227         addToolBar(DEFAULT_GROUP, DEFAULT_LAYER, toolBar);
228     } //}}}
229 
230     //{{{ addToolBar() method
231     /**
232      * Adds a tool bar to this view.
233      * @param group The tool bar group to add to
234      * @param toolBar The tool bar
235      * @see org.gjt.sp.jedit.gui.ToolBarManager
236      * @since jEdit 4.0pre7
237      */
238     public void addToolBar(int group, Component toolBar)
239     {
240         addToolBar(group, DEFAULT_LAYER, toolBar);
241     } //}}}
242 
243     //{{{ addToolBar() method
244     /**
245      * Adds a tool bar to this view.
246      * @param group The tool bar group to add to
247      * @param layer The layer of the group to add to
248      * @param toolBar The tool bar
249      * @see org.gjt.sp.jedit.gui.ToolBarManager
250      * @since jEdit 4.0pre7
251      */
252     public void addToolBar(int group, int layer, Component toolBar)
253     {
254         toolBarManager.addToolBar(group, layer, toolBar);
255         getRootPane().revalidate();
256     } //}}}
257 
258     //{{{ removeToolBar() method
259     /**
260      * Removes a tool bar from this view.
261      * @param toolBar The tool bar
262      */
263     public void removeToolBar(Component toolBar)
264     {
265         if (toolBarManager == null) return;
266         if (toolBar == null) return;
267         toolBarManager.removeToolBar(toolBar);
268         getRootPane().revalidate();
269     } //}}}
270 
271     //{{{ showWaitCursor() method
272     /**
273      * Shows the wait cursor. This method and
274      * {@link #hideWaitCursor()} are implemented using a reference
275      * count of requests for wait cursors, so that nested calls work
276      * correctly; however, you should be careful to use these methods in
277      * tandem.<p>
278      *
279      * To ensure that {@link #hideWaitCursor()} is always called
280      * after a {@link #showWaitCursor()}, use a
281      * <code>try</code>/<code>finally</code> block, like this:
282      * <pre>try
283      *{
284      *    view.showWaitCursor();
285      *    // ...
286      *}
287      *finally
288      *{
289      *    view.hideWaitCursor();
290      *}</pre>
291      */
292     public synchronized void showWaitCursor()
293     {
294         if(waitCount++ == 0)
295         {
296             Cursor cursor = Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR);
297             setCursor(cursor);
298             EditPane[] editPanes = getEditPanes();
299             for(int i = 0; i < editPanes.length; i++)
300             {
301                 EditPane editPane = editPanes[i];
302                 editPane.getTextArea().getPainter()
303                     .setCursor(cursor);
304             }
305         }
306     } //}}}
307 
308     //{{{ hideWaitCursor() method
309     /**
310      * Hides the wait cursor.
311      */
312     public synchronized void hideWaitCursor()
313     {
314         if(waitCount > 0)
315             waitCount--;
316 
317         if(waitCount == 0)
318         {
319             // still needed even though glass pane
320             // has a wait cursor
321             Cursor cursor = Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR);
322             setCursor(cursor);
323             cursor = Cursor.getPredefinedCursor(Cursor.TEXT_CURSOR);
324             EditPane[] editPanes = getEditPanes();
325             for(int i = 0; i < editPanes.length; i++)
326             {
327                 EditPane editPane = editPanes[i];
328                 editPane.getTextArea().getPainter()
329                     .setCursor(cursor);
330             }
331         }
332     } //}}}
333 
334     //{{{ getSearchBar() method
335     /**
336      * Returns the search bar.
337      * @since jEdit 2.4pre4
338      */
339     public final SearchBar getSearchBar()
340     {
341         return searchBar;
342     } //}}}
343 
344     //{{{ getActionBar() method
345     /**
346      * Returns the action bar.
347      * @since jEdit 4.2pre3
348      */
349     public final ActionBar getActionBar()
350     {
351         return actionBar;
352     } //}}}
353 
354     //{{{ getStatus() method
355     /**
356      * Returns the status bar. The
357      * {@link org.gjt.sp.jedit.gui.StatusBar#setMessage(String)} and
358      * {@link org.gjt.sp.jedit.gui.StatusBar#setMessageAndClear(String)} methods can
359      * be called on the return value of this method to display status
360      * information to the user.
361      * @since jEdit 3.2pre2
362      */
363     public StatusBar getStatus()
364     {
365         return status;
366     } //}}}
367 
368     //{{{ quickIncrementalSearch() method
369     /**
370      * Quick search.
371      * @since jEdit 4.0pre3
372      */
373     public void quickIncrementalSearch(boolean word)
374     {
375         if(searchBar == null)
376             searchBar = new SearchBar(this,true);
377         if(searchBar.getParent() == null)
378             addToolBar(TOP_GROUP,SEARCH_BAR_LAYER,searchBar);
379 
380         searchBar.setHyperSearch(false);
381 
382         JEditTextArea textArea = getTextArea();
383 
384         if(word)
385         {
386             String   text = textArea.getSelectedText();
387             if(text == null)
388             {
389                 textArea.selectWord();
390                 text = textArea.getSelectedText();
391             }
392             else if(text.indexOf('\n') != -1)
393                 text = null;
394 
395             if(text != null && SearchAndReplace.getRegexp())
396                 text = SearchAndReplace.escapeRegexp(text,false);
397 
398             searchBar.getField().setText(text);
399         }
400 
401         searchBar.getField().requestFocus();
402         searchBar.getField().selectAll();
403     } //}}}
404 
405     //{{{ quickHyperSearch() method
406     /**
407      * Quick HyperSearch.
408      * @since jEdit 4.0pre3
409      */
410     public void quickHyperSearch(boolean word)
411     {
412         JEditTextArea textArea = getTextArea();
413 
414         if(word)
415         {
416             String   text = textArea.getSelectedText();
417             if(text == null)
418             {
419                 textArea.selectWord();
420                 text = textArea.getSelectedText();
421             }
422 
423             if(text != null && text.indexOf('\n') == -1)
424             {
425                 if(SearchAndReplace.getRegexp())
426                 {
427                     text = SearchAndReplace.escapeRegexp(
428                         text,false);
429                 }
430 
431                 HistoryModel.getModel("find").addItem(text);
432                 SearchAndReplace.setSearchString(text);
433                 SearchAndReplace.setSearchFileSet(new CurrentBufferSet());
434                 SearchAndReplace.hyperSearch(this);
435 
436                 return;
437             }
438         }
439 
440         if(searchBar == null)
441             searchBar = new SearchBar(this,true);
442         if(searchBar.getParent() == null)
443             addToolBar(TOP_GROUP,SEARCH_BAR_LAYER,searchBar);
444 
445         searchBar.setHyperSearch(true);
446         searchBar.getField().setText(null);
447         searchBar.getField().requestFocus();
448         searchBar.getField().selectAll();
449     } //}}}
450 
451     //{{{ actionBar() method
452     /**
453      * Shows the action bar if needed, and sends keyboard focus there.
454      * @since jEdit 4.2pre1
455      */
456     public void actionBar()
457     {
458         if(actionBar == null)
459             actionBar = new ActionBar(this,true);
460         if(actionBar.getParent() == null)
461             addToolBar(BOTTOM_GROUP,ACTION_BAR_LAYER,actionBar);
462 
463         actionBar.goToActionBar();
464     } //}}}
465 
466     //}}}
467 
468     //{{{ Input handling
469 
470     //{{{ getKeyEventInterceptor() method
471     /**
472      * Returns the listener that will handle all key events in this
473      * view, if any.
474      */
475     public KeyListener getKeyEventInterceptor()
476     {
477         return inputHandler.getKeyEventInterceptor();
478     } //}}}
479 
480     //{{{ setKeyEventInterceptor() method
481     /**
482      * Sets the listener that will handle all key events in this
483      * view. For example, the complete word command uses this so
484      * that all key events are passed to the word list popup while
485      * it is visible.
486      * @param listener The key event interceptor.
487      */
488     public void setKeyEventInterceptor(KeyListener listener)
489     {
490         inputHandler.setKeyEventInterceptor(listener);
491     } //}}}
492 
493     //{{{ getInputHandler() method
494     /**
495      * Returns the input handler.
496      */
497     public InputHandler getInputHandler()
498     {
499         return inputHandler;
500     } //}}}
501 
502 
503 
504     //{{{ setInputHandler() method
505     /**
506      * Sets the input handler.
507      * @param inputHandler The new input handler
508      */
509     public void setInputHandler(InputHandler inputHandler)
510     {
511         this.inputHandler = inputHandler;
512     } //}}}
513 
514     //{{{ getMacroRecorder() method
515     /**
516      * Returns the macro recorder.
517      */
518     public Macros.Recorder getMacroRecorder()
519     {
520         return recorder;
521     } //}}}
522 
523     //{{{ setMacroRecorder() method
524     /**
525      * Sets the macro recorder.
526      * @param recorder The macro recorder
527      */
528     public void setMacroRecorder(Macros.Recorder recorder)
529     {
530         this.recorder = recorder;
531     } //}}}
532 
533     //{{{ processKeyEvent() method
534     /**
535      * Forwards key events directly to the input handler.
536      * This is slightly faster than using a KeyListener
537      * because some Swing overhead is avoided.
538      */
539     public void processKeyEvent(KeyEvent evt)
540     {
541         inputHandler.processKeyEvent(evt,VIEW, false);
542         if(!evt.isConsumed())
543             super.processKeyEvent(evt);
544     } //}}}
545 
546     //{{{ processKeyEvent() method
547     /**
548      * Forwards key events directly to the input handler.
549      * This is slightly faster than using a KeyListener
550      * because some Swing overhead is avoided.
551      */
552     public void processKeyEvent(KeyEvent evt, boolean calledFromTextArea)
553     {
554         processKeyEvent(evt,calledFromTextArea
555             ? TEXT_AREA
556             : VIEW);
557     } //}}}
558 
559     //{{{ processKeyEvent() method
560     public static final int VIEW = 0;
561     public static final int TEXT_AREA = 1;
562     public static final int ACTION_BAR = 2;
563     /**
564      * Forwards key events directly to the input handler.
565      * This is slightly faster than using a KeyListener
566      * because some Swing overhead is avoided.
567      */
568     public void processKeyEvent(KeyEvent evt, int from)
569     {
570         processKeyEvent(evt,from,false);
571     }
572     /**
573      * Forwards key events directly to the input handler.
574      * This is slightly faster than using a KeyListener
575      * because some Swing overhead is avoided.
576      * @deprecated do not use, try {@link org.gjt.sp.jedit.gui.InputHandler#processKeyEvent(java.awt.event.KeyEvent, int, boolean)}
577      */
578     public void processKeyEvent(KeyEvent evt, int from, boolean global)
579     {
580         inputHandler.processKeyEvent(evt, from, global);
581         if(!evt.isConsumed())
582             super.processKeyEvent(evt);
583     } //}}}
584 
585 
586     //}}}
587 
588     //{{{ Buffers, edit panes, split panes
589 
590     //{{{ splitHorizontally() method
591     /**
592      * Splits the view horizontally.
593      * @since jEdit 4.1pre2
594      */
595     public EditPane splitHorizontally()
596     {
597         return split(JSplitPane.VERTICAL_SPLIT);
598     } //}}}
599 
600     //{{{ splitVertically() method
601     /**
602      * Splits the view vertically.
603      * @since jEdit 4.1pre2
604      */
605     public EditPane splitVertically()
606     {
607         return split(JSplitPane.HORIZONTAL_SPLIT);
608     } //}}}
609 
610     //{{{ split() method
611     /**
612      * Splits the view.
613      * @since jEdit 4.1pre2
614      */
615     public EditPane split(int orientation)
616     {
617         PerspectiveManager.setPerspectiveDirty(true);
618 
619         editPane.saveCaretInfo();
620         EditPane oldEditPane = editPane;
621         setEditPane(createEditPane(oldEditPane.getBuffer()));
622         editPane.loadCaretInfo();
623 
624         JComponent oldParent = (JComponent)oldEditPane.getParent();
625 
626         final JSplitPane newSplitPane = new JSplitPane(orientation,
627                                    jEdit.getBooleanProperty("appearance.continuousLayout"));
628         newSplitPane.setOneTouchExpandable(true);
629         newSplitPane.setBorder(null);
630         newSplitPane.setMinimumSize(new Dimension(0,0));
631         newSplitPane.setResizeWeight(0.5);
632 
633         int parentSize = orientation == JSplitPane.VERTICAL_SPLIT
634             ? oldEditPane.getHeight() : oldEditPane.getWidth();
635         final int dividerPosition = (int)((parentSize
636             - newSplitPane.getDividerSize()) * 0.5);
637         newSplitPane.setDividerLocation(dividerPosition);
638 
639         if(oldParent instanceof JSplitPane)
640         {
641             JSplitPane oldSplitPane = (JSplitPane)oldParent;
642             int dividerPos = oldSplitPane.getDividerLocation();
643 
644             Component left = oldSplitPane.getLeftComponent();
645 
646             if(left == oldEditPane)
647                 oldSplitPane.setLeftComponent(newSplitPane);
648             else
649                 oldSplitPane.setRightComponent(newSplitPane);
650 
651             newSplitPane.setLeftComponent(oldEditPane);
652             newSplitPane.setRightComponent(editPane);
653 
654             oldSplitPane.setDividerLocation(dividerPos);
655         }
656         else
657         {
658             splitPane = newSplitPane;
659 
660             newSplitPane.setLeftComponent(oldEditPane);
661             newSplitPane.setRightComponent(editPane);
662 
663             oldParent.add(newSplitPane,0);
664             oldParent.revalidate();
665         }
666 
667         SwingUtilities.invokeLater(new Runnable  ()
668         {
669             public void run()
670             {
671                 newSplitPane.setDividerLocation(dividerPosition);
672             }
673         });
674 
675         editPane.focusOnTextArea();
676 
677         return editPane;
678     } //}}}
679 
680     //{{{ unsplit() method
681     /**
682      * Unsplits the view.
683      * @since jEdit 2.3pre2
684      */
685     public void unsplit()
686     {
687         if(splitPane != null)
688         {
689             lastSplitConfig = getSplitConfig();
690 
691             PerspectiveManager.setPerspectiveDirty(true);
692 
693             EditPane[] editPanes = getEditPanes();
694             for(int i = 0; i < editPanes.length; i++)
695             {
696                 EditPane _editPane = editPanes[i];
697                 if(editPane != _editPane)
698                     _editPane.close();
699             }
700 
701             JComponent parent = (JComponent)splitPane.getParent();
702 
703             parent.remove(splitPane);
704             parent.add(editPane,0);
705             parent.revalidate();
706 
707             splitPane = null;
708             updateTitle();
709 
710             editPane.focusOnTextArea();
711         }
712         else
713             getToolkit().beep();
714     } //}}}
715 
716     //{{{ unsplitCurrent() method
717     /**
718      * Removes the current split.
719      * @since jEdit 2.3pre2
720      */
721     public void unsplitCurrent()
722     {
723         if(splitPane != null)
724         {
725             lastSplitConfig = getSplitConfig();
726 
727             PerspectiveManager.setPerspectiveDirty(true);
728 
729             // find first split pane parenting current edit pane
730             Component comp = editPane;
731             while(!(comp instanceof JSplitPane))
732             {
733                 comp = comp.getParent();
734             }
735 
736             // get rid of any edit pane that is a child
737             // of the current edit pane's parent splitter
738             EditPane[] editPanes = getEditPanes();
739             for(int i = 0; i < editPanes.length; i++)
740             {
741                 EditPane _editPane = editPanes[i];
742                 if(GUIUtilities.isAncestorOf(comp,_editPane)
743                     && _editPane != editPane)
744                     _editPane.close();
745             }
746 
747             JComponent parent = (JComponent)comp.getParent();
748 
749             if(parent instanceof JSplitPane)
750             {
751                 JSplitPane parentSplit = (JSplitPane)parent;
752                 int pos = parentSplit.getDividerLocation();
753                 if(parentSplit.getLeftComponent() == comp)
754                     parentSplit.setLeftComponent(editPane);
755                 else
756                     parentSplit.setRightComponent(editPane);
757                 parentSplit.setDividerLocation(pos);
758             }
759             else
760             {
761                 parent.remove(comp);
762                 parent.add(editPane,0);
763                 splitPane = null;
764             }
765 
766             parent.revalidate();
767 
768             updateTitle();
769 
770             editPane.focusOnTextArea();
771         }
772         else
773             getToolkit().beep();
774     } //}}}
775 
776     //{{{ resplit() method
777     /**
778      * Restore the split configuration as it was before unsplitting.
779      *
780      * @since jEdit 4.3pre1
781      */
782     public void resplit()
783     {
784         if(lastSplitConfig == null)
785             getToolkit().beep();
786         else
787             setSplitConfig(null,lastSplitConfig);
788     } //}}}
789 
790     //{{{ nextTextArea() method
791     /**
792      * Moves keyboard focus to the next text area.
793      * @since jEdit 2.7pre4
794      */
795     public void nextTextArea()
796     {
797         EditPane[] editPanes = getEditPanes();
798         for(int i = 0; i < editPanes.length; i++)
799         {
800             if(editPane == editPanes[i])
801             {
802                 if(i == editPanes.length - 1)
803                     editPanes[0].focusOnTextArea();
804                 else
805                     editPanes[i+1].focusOnTextArea();
806                 break;
807             }
808         }
809     } //}}}
810 
811     //{{{ prevTextArea() method
812     /**
813      * Moves keyboard focus to the previous text area.
814      * @since jEdit 2.7pre4
815      */
816     public void prevTextArea()
817     {
818         EditPane[] editPanes = getEditPanes();
819         for(int i = 0; i < editPanes.length; i++)
820         {
821             if(editPane == editPanes[i])
822             {
823                 if(i == 0)
824                     editPanes[editPanes.length - 1].focusOnTextArea();
825                 else
826                     editPanes[i-1].focusOnTextArea();
827                 break;
828             }
829         }
830     } //}}}
831 
832     //{{{ getSplitPane() method
833     /**
834      * Returns the top-level split pane, if any.
835      * @since jEdit 2.3pre2
836      */
837     public JSplitPane getSplitPane()
838     {
839         return splitPane;
840     } //}}}
841 
842     //{{{ getBuffer() method
843     /**
844      * Returns the current edit pane's buffer.
845      */
846     public Buffer getBuffer()
847     {
848         if(editPane == null)
849             return null;
850         else
851             return editPane.getBuffer();
852     } //}}}
853 
854     //{{{ setBuffer() method
855     /**
856      * Sets the current edit pane's buffer.
857      */
858     public void setBuffer(Buffer buffer)
859     {
860         editPane.setBuffer(buffer);
861     } //}}}
862 
863     //{{{ goToBuffer() method
864     /**
865      * If this buffer is open in one of the view's edit panes, sets focus
866      * to that edit pane. Otherwise, opens the buffer in the currently
867      * active edit pane.
868      * @param buffer The buffer
869      * @since jEdit 4.2pre1
870      */
871     public EditPane goToBuffer(Buffer buffer)
872     {
873         if(editPane.getBuffer() == buffer
874             && editPane.getTextArea().getVisibleLines() > 1)
875         {
876             editPane.focusOnTextArea();
877             return editPane;
878         }
879 
880         EditPane[] editPanes = getEditPanes();
881         for(int i = 0; i < editPanes.length; i++)
882         {
883             EditPane ep = editPanes[i];
884             if(ep.getBuffer() == buffer
885                 /* ignore zero-height splits, etc */
886                 && ep.getTextArea().getVisibleLines() > 1)
887             {
888                 setEditPane(ep);
889                 ep.focusOnTextArea();
890                 return ep;
891             }
892         }
893 
894         setBuffer(buffer);
895         return editPane;
896     } //}}}
897 
898     //{{{ getTextArea() method
899     /**
900      * Returns the current edit pane's text area.
901      */
902     public JEditTextArea getTextArea()
903     {
904         if(editPane == null)
905             return null;
906         else
907             return editPane.getTextArea();
908     } //}}}
909 
910     //{{{ getEditPane() method
911     /**
912      * Returns the current edit pane.
913      * @since jEdit 2.5pre2
914      */
915     public EditPane getEditPane()
916     {
917         return editPane;
918     } //}}}
919 
920     //{{{ getEditPanes() method
921     /**
922      * Returns all edit panes.
923      * @since jEdit 2.5pre2
924      */
925     public EditPane[] getEditPanes()
926     {
927         if(splitPane == null)
928         {
929             EditPane[] ep = { editPane };
930             return ep;
931         }
932         else
933         {
934             List  <EditPane> vec = new ArrayList<EditPane>();
935             getEditPanes(vec,splitPane);
936             EditPane[] ep = new EditPane[vec.size()];
937             vec.toArray(ep);
938             return ep;
939         }
940     } //}}}
941 
942     //{{{ getViewConfig() method
943     /**
944      * @since jEdit 4.2pre1
945      */
946     public ViewConfig getViewConfig()
947     {
948         ViewConfig config = new ViewConfig();
949         config.plainView = isPlainView();
950         config.splitConfig = getSplitConfig();
951         config.extState = getExtendedState();
952         String   prefix = config.plainView ? "plain-view" : "view";
953         switch (config.extState)
954         {
955             case Frame.MAXIMIZED_BOTH:
956             case Frame.ICONIFIED:
957                 config.x = jEdit.getIntegerProperty(prefix + ".x",getX());
958                 config.y = jEdit.getIntegerProperty(prefix + ".y",getY());
959                 config.width = jEdit.getIntegerProperty(prefix + ".width",getWidth());
960                 config.height = jEdit.getIntegerProperty(prefix + ".height",getHeight());
961                 break;
962 
963             case Frame.MAXIMIZED_VERT:
964                 config.x = getX();
965                 config.y = jEdit.getIntegerProperty(prefix + ".y",getY());
966                 config.width = getWidth();
967                 config.height = jEdit.getIntegerProperty(prefix + ".height",getHeight());
968                 break;
969 
970             case Frame.MAXIMIZED_HORIZ:
971                 config.x = jEdit.getIntegerProperty(prefix + ".x",getX());
972                 config.y = getY();
973                 config.width = jEdit.getIntegerProperty(prefix + ".width",getWidth());
974                 config.height = getHeight();
975                 break;
976 
977             case Frame.NORMAL:
978             default:
979                 config.x = getX();
980                 config.y = getY();
981                 config.width = getWidth();
982                 config.height = getHeight();
983                 break;
984         }
985 
986         config.top = dockableWindowManager.getTopDockingArea().getCurrent();
987         config.left = dockableWindowManager.getLeftDockingArea().getCurrent();
988         config.bottom = dockableWindowManager.getBottomDockingArea().getCurrent();
989         config.right = dockableWindowManager.getRightDockingArea().getCurrent();
990 
991         config.topPos = dockableWindowManager.getTopDockingArea().getDimension();
992         config.leftPos = dockableWindowManager.getLeftDockingArea().getDimension();
993         config.bottomPos = dockableWindowManager.getBottomDockingArea().getDimension();
994         config.rightPos = dockableWindowManager.getRightDockingArea().getDimension();
995 
996         return config;
997     } //}}}
998 
999     //}}}
1000
1001    //{{{ isClosed() method
1002    /**
1003     * Returns true if this view has been closed with
1004     * {@link jEdit#closeView(View)}.
1005     */
1006    public boolean isClosed()
1007    {
1008        return closed;
1009    } //}}}
1010
1011    //{{{ isPlainView() method
1012    /**
1013     * Returns true if this is an auxilliary view with no dockable windows.
1014     * @since jEdit 4.1pre2
1015     */
1016    public boolean isPlainView()
1017    {
1018        return plainView;
1019    } //}}}
1020
1021    //{{{ getNext() method
1022    /**
1023     * Returns the next view in the list.
1024     */
1025    public View getNext()
1026    {
1027        return next;
1028    } //}}}
1029
1030    //{{{ getPrev() method
1031    /**
1032     * Returns the previous view in the list.
1033     */
1034    public View getPrev()
1035    {
1036        return prev;
1037    } //}}}
1038
1039    //{{{ handleMessage() method
1040    public void handleMessage(EBMessage msg)
1041    {
1042        if(msg instanceof PropertiesChanged)
1043            propertiesChanged();
1044        else if(msg instanceof SearchSettingsChanged)
1045        {
1046            if(searchBar != null)
1047                searchBar.update();
1048        }
1049        else if(msg instanceof BufferUpdate)
1050            handleBufferUpdate((BufferUpdate)msg);
1051        else if(msg instanceof EditPaneUpdate)
1052            handleEditPaneUpdate((EditPaneUpdate)msg);
1053    } //}}}
1054
1055    //{{{ getMinimumSize() method
1056    public Dimension getMinimumSize()
1057    {
1058        return new Dimension(0,0);
1059    } //}}}
1060
1061    //{{{ setWaitSocket() method
1062    /**
1063     * This socket is closed when the buffer is closed.
1064     */
1065    public void setWaitSocket(Socket   waitSocket)
1066    {
1067        this.waitSocket = waitSocket;
1068    } //}}}
1069
1070    //{{{ toString() method
1071    public String   toString()
1072    {
1073        return getClass().getName() + '['
1074            + (jEdit.getActiveView() == this
1075            ? "active" : "inactive")
1076            + ']';
1077    } //}}}
1078
1079    //{{{ updateTitle() method
1080    /**
1081     * Updates the title bar.
1082     */
1083    public void updateTitle()
1084    {
1085        List  <Buffer> buffers = new ArrayList<Buffer>();
1086        EditPane[] editPanes = getEditPanes();
1087        for(int i = 0; i < editPanes.length; i++)
1088        {
1089            Buffer buffer = editPanes[i].getBuffer();
1090            if(buffers.indexOf(buffer) == -1)
1091                buffers.add(buffer);
1092        }
1093
1094        StringBuilder   title = new StringBuilder  ();
1095
1096        /* On Mac OS X, apps are not supposed to show their name in the
1097        title bar. */
1098        if(!OperatingSystem.isMacOS())
1099            title.append(jEdit.getProperty("view.title"));
1100
1101        boolean unsavedChanges = false;
1102
1103        for(int i = 0; i < buffers.size(); i++)
1104        {
1105            if(i != 0)
1106                title.append(", ");
1107
1108            Buffer buffer = buffers.get(i);
1109            title.append((showFullPath && !buffer.isNewFile())
1110                ? buffer.getPath() : buffer.getName());
1111            if(buffer.isDirty())
1112            {
1113                unsavedChanges = true;
1114                title.append(jEdit.getProperty("view.title.dirty"));
1115            }
1116        }
1117
1118        setTitle(title.toString());
1119
1120        /* On MacOS X, the close box is shown in a different color if
1121        an app has unsaved changes. For details, see
1122        http://developer.apple.com/qa/qa2001/qa1146.html */
1123        final String   WINDOW_MODIFIED = "windowModified";
1124        getRootPane().putClientProperty(WINDOW_MODIFIED,
1125            unsavedChanges);
1126    } //}}}
1127
1128
1129    public Component getPrefixFocusOwner()
1130    {
1131        return prefixFocusOwner;
1132    }
1133
1134
1135    public void setPrefixFocusOwner(Component prefixFocusOwner)
1136    {
1137        this.prefixFocusOwner = prefixFocusOwner;
1138    }
1139
1140    //{{{ Package-private members
1141    View prev;
1142    View next;
1143
1144    //{{{ View constructor
1145    View(Buffer buffer, ViewConfig config)
1146    {
1147        plainView = config.plainView;
1148
1149        enableEvents(AWTEvent.KEY_EVENT_MASK);
1150
1151        setIconImage(GUIUtilities.getEditorIcon());
1152
1153        dockableWindowManager = new DockableWindowManager(this,
1154            DockableWindowFactory.getInstance(),config);
1155
1156        topToolBars = new JPanel(new VariableGridLayout(
1157            VariableGridLayout.FIXED_NUM_COLUMNS,
1158            1));
1159        bottomToolBars = new JPanel(new VariableGridLayout(
1160            VariableGridLayout.FIXED_NUM_COLUMNS,
1161            1));
1162
1163        toolBarManager = new ToolBarManager(topToolBars, bottomToolBars);
1164
1165        status = new StatusBar(this);
1166
1167        inputHandler = new DefaultInputHandler(this,(DefaultInputHandler)
1168            jEdit.getInputHandler());
1169
1170        setSplitConfig(buffer,config.splitConfig);
1171
1172        getContentPane().add(BorderLayout.CENTER,dockableWindowManager);
1173
1174        dockableWindowManager.init();
1175
1176        // tool bar and status bar gets added in propertiesChanged()
1177        // depending in the 'tool bar alternate layout' setting.
1178        propertiesChanged();
1179
1180        setDefaultCloseOperation(DO_NOTHING_ON_CLOSE);
1181        addWindowListener(new WindowHandler());
1182
1183        setFocusTraversalPolicy(new MyFocusTraversalPolicy());
1184
1185        EditBus.addToBus(this);
1186
1187        GUIUtilities.addSizeSaver(this, null, plainView ? "plain-view" : "view");
1188    } //}}}
1189
1190    //{{{ close() method
1191    void close()
1192    {
1193        closed = true;
1194
1195        // save dockable window geometry, and close 'em
1196        dockableWindowManager.close();
1197
1198        EditBus.removeFromBus(this);
1199        dispose();
1200
1201        EditPane[] editPanes = getEditPanes();
1202        for(int i = 0; i < editPanes.length; i++)
1203            editPanes[i].close();
1204
1205        // null some variables so that retaining references
1206        // to closed views won't hurt as much.
1207        toolBarManager = null;
1208        toolBar = null;
1209        searchBar = null;
1210        splitPane = null;
1211        inputHandler = null;
1212        recorder = null;
1213
1214        getContentPane().removeAll();
1215
1216        // notify clients with -wait
1217        if(waitSocket != null)
1218        {
1219            try
1220            {
1221                waitSocket.getOutputStream().write('\0');
1222                waitSocket.getOutputStream().flush();
1223                waitSocket.getInputStream().close();
1224                waitSocket.getOutputStream().close();
1225                waitSocket.close();
1226            }
1227            catch(IOException   io)
1228            {
1229                //Log.log(Log.ERROR,this,io);
1230            }
1231        }
1232    } //}}}
1233
1234    //}}}
1235
1236    //{{{ Private members
1237
1238    //{{{ Instance variables
1239    private boolean closed;
1240
1241    private DockableWindowManager dockableWindowManager;
1242
1243    private JPanel topToolBars;
1244    private JPanel bottomToolBars;
1245    private ToolBarManager toolBarManager;
1246
1247    private Box toolBar;
1248    private SearchBar searchBar;
1249    private ActionBar actionBar;
1250
1251    private EditPane editPane;
1252    private JSplitPane splitPane;
1253    private String   lastSplitConfig;
1254
1255    private StatusBar status;
1256
1257    private InputHandler inputHandler;
1258    private Macros.Recorder recorder;
1259    private Component prefixFocusOwner;
1260
1261    private int waitCount;
1262
1263    private boolean showFullPath;
1264
1265    private boolean plainView;
1266
1267    private Socket   waitSocket;
1268    //}}}
1269
1270    //{{{ getEditPanes() method
1271    private static void getEditPanes(List  <EditPane> vec, Component comp)
1272    {
1273        if(comp instanceof EditPane)
1274            vec.add((EditPane) comp);
1275        else if(comp instanceof JSplitPane)
1276        {
1277            JSplitPane split = (JSplitPane)comp;
1278            getEditPanes(vec,split.getLeftComponent());
1279            getEditPanes(vec,split.getRightComponent());
1280        }
1281    } //}}}
1282
1283    //{{{ getSplitConfig() method
1284    private String   getSplitConfig()
1285    {
1286        StringBuilder   splitConfig = new StringBuilder  ();
1287
1288        if(splitPane != null)
1289            getSplitConfig(splitPane,splitConfig);
1290        else
1291        {
1292            splitConfig.append('"');
1293            splitConfig.append(MiscUtilities.charsToEscapes(
1294                getBuffer().getPath()));
1295            splitConfig.append("\" buffer");
1296        }
1297
1298        return splitConfig.toString();
1299    } //}}}
1300
1301    //{{{ getSplitConfig() method
1302    /*
1303     * The split config is recorded in a simple RPN "language".
1304     */
1305    private static void getSplitConfig(JSplitPane splitPane,
1306        StringBuilder   splitConfig)
1307    {
1308        Component right = splitPane.getRightComponent();
1309        if(right instanceof JSplitPane)
1310            getSplitConfig((JSplitPane)right,splitConfig);
1311        else
1312        {
1313            splitConfig.append('"');
1314            splitConfig.append(MiscUtilities.charsToEscapes(
1315                ((EditPane)right).getBuffer().getPath()));
1316            splitConfig.append("\" buffer");
1317        }
1318
1319        splitConfig.append(' ');
1320
1321        Component left = splitPane.getLeftComponent();
1322        if(left instanceof JSplitPane)
1323            getSplitConfig((JSplitPane)left,splitConfig);
1324        else
1325        {
1326            splitConfig.append('"');
1327            splitConfig.append(MiscUtilities.charsToEscapes(
1328                ((EditPane)left).getBuffer().getPath()));
1329            splitConfig.append("\" buffer");
1330        }
1331
1332        splitConfig.append(' ');
1333        splitConfig.append(splitPane.getDividerLocation());
1334        splitConfig.append(' ');
1335        splitConfig.append(splitPane.getOrientation()
1336            == JSplitPane.VERTICAL_SPLIT ? "vertical" : "horizontal");
1337    } //}}}
1338
1339    //{{{ setSplitConfig() method
1340    private void setSplitConfig(Buffer buffer, String   splitConfig)
1341    {
1342        if(editPane != null)
1343            dockableWindowManager.remove(editPane);
1344
1345        if(splitPane != null)
1346            dockableWindowManager.remove(splitPane);
1347
1348        try
1349        {
1350            Component comp = restoreSplitConfig(buffer,splitConfig);
1351            dockableWindowManager.add(comp,0);
1352        }
1353        catch(IOException   e)
1354        {
1355            // this should never throw an exception.
1356            throw new InternalError  ();
1357        }
1358
1359        dockableWindowManager.revalidate();
1360        dockableWindowManager.repaint();
1361    } //}}}
1362
1363    //{{{ restoreSplitConfig() method
1364    private Component restoreSplitConfig(Buffer buffer, String   splitConfig)
1365        throws IOException  
1366    // this is where checked exceptions piss me off. this method only uses
1367    // a StringReader which can never throw an exception...
1368    {
1369        if(buffer != null)
1370            return editPane = createEditPane(buffer);
1371        else if(splitConfig == null)
1372            return editPane = createEditPane(jEdit.getFirstBuffer());
1373
1374        Buffer[] buffers = jEdit.getBuffers();
1375
1376        Stack stack = new Stack();
1377
1378        // we create a stream tokenizer for parsing a simple
1379        // stack-based language
1380        StreamTokenizer   st = new StreamTokenizer  (new StringReader  (
1381            splitConfig));
1382        st.whitespaceChars(0,' ');
1383        /* all printable ASCII characters */
1384        st.wordChars('#','~');
1385        st.commentChar('!');
1386        st.quoteChar('"');
1387        st.eolIsSignificant(false);
1388        boolean continuousLayout = jEdit.getBooleanProperty("appearance.continuousLayout");
1389loop:       while (true)
1390        {
1391            switch(st.nextToken())
1392            {
1393            case StreamTokenizer.TT_EOF:
1394                break loop;
1395            case StreamTokenizer.TT_WORD:
1396                if(st.sval.equals("vertical") ||
1397                    st.sval.equals("horizontal"))
1398                {
1399                    int orientation
1400                        = (st.sval.equals("vertical")
1401                        ? JSplitPane.VERTICAL_SPLIT
1402                        : JSplitPane.HORIZONTAL_SPLIT);
1403                    int divider = ((Integer  )stack.pop())
1404                        .intValue();
1405                    stack.push(splitPane = new JSplitPane(
1406                        orientation,
1407                        continuousLayout,
1408                        (Component)stack.pop(),
1409                        (Component)stack.pop()));
1410                    splitPane.setOneTouchExpandable(true);
1411                    splitPane.setBorder(null);
1412                    splitPane.setMinimumSize(
1413                        new Dimension(0,0));
1414                    splitPane.setDividerLocation(divider);
1415                }
1416                else if(st.sval.equals("buffer"))
1417                {
1418                    Object   obj = stack.pop();
1419                    if(obj instanceof Integer  )
1420                    {
1421                        int index = ((Integer  )obj).intValue();
1422                        if(index >= 0 && index < buffers.length)
1423                            buffer = buffers[index];
1424                    }
1425                    else if(obj instanceof String  )
1426                    {
1427                        String   path = (String  )obj;
1428                        buffer = jEdit.getBuffer(path);
1429                    }
1430
1431                    if(buffer == null)
1432                        buffer = jEdit.getFirstBuffer();
1433
1434                    stack.push(editPane = createEditPane(
1435                        buffer));
1436                }
1437                break;
1438            case StreamTokenizer.TT_NUMBER:
1439                stack.push((int)st.nval);
1440                break;
1441            case '"':
1442                stack.push(st.sval);
1443                break;
1444            }
1445        }
1446
1447        updateGutterBorders();
1448
1449        return (Component)stack.peek();
1450    } //}}}
1451
1452    //{{{ propertiesChanged() method
1453    /**
1454     * Reloads various settings from the properties.
1455     */
1456    private void propertiesChanged()
1457    {
1458        setJMenuBar(GUIUtilities.loadMenuBar("view.mbar"));
1459
1460        loadToolBars();
1461
1462        showFullPath = jEdit.getBooleanProperty("view.showFullPath");
1463        updateTitle();
1464
1465        status.propertiesChanged();
1466
1467        removeToolBar(status);
1468        getContentPane().remove(status);
1469
1470        if(jEdit.getBooleanProperty("view.toolbar.alternateLayout"))
1471        {
1472            getContentPane().add(BorderLayout.NORTH,topToolBars);
1473            getContentPane().add(BorderLayout.SOUTH,bottomToolBars);
1474            if(!plainView && jEdit.getBooleanProperty("view.status.visible"))
1475                addToolBar(BOTTOM_GROUP,STATUS_BAR_LAYER,status);
1476        }
1477        else
1478        {
1479            dockableWindowManager.add(topToolBars,
1480                DockableLayout.TOP_TOOLBARS,0);
1481            dockableWindowManager.add(bottomToolBars,
1482                DockableLayout.BOTTOM_TOOLBARS,0);
1483            if(!plainView && jEdit.getBooleanProperty("view.status.visible"))
1484                getContentPane().add(BorderLayout.SOUTH,status);
1485        }
1486
1487        getRootPane().revalidate();
1488
1489        if (splitPane != null)
1490            GUIUtilities.initContinuousLayout(splitPane);
1491        //SwingUtilities.updateComponentTreeUI(getRootPane());
1492    } //}}}
1493
1494    //{{{ loadToolBars() method
1495    private void loadToolBars()
1496    {
1497        if(jEdit.getBooleanProperty("view.showToolbar") && !plainView)
1498        {
1499            if(toolBar != null)
1500                toolBarManager.removeToolBar(toolBar);
1501
1502            toolBar = GUIUtilities.loadToolBar("view.toolbar");
1503
1504            addToolBar(TOP_GROUP, SYSTEM_BAR_LAYER, toolBar);
1505        }
1506        else if(toolBar != null)
1507        {
1508            removeToolBar(toolBar);
1509            toolBar = null;
1510        }
1511
1512        if(searchBar != null)
1513            removeToolBar(searchBar);
1514
1515        if(jEdit.getBooleanProperty("view.showSearchbar") && !plainView)
1516        {
1517            if(searchBar == null)
1518                searchBar = new SearchBar(this,false);
1519            searchBar.propertiesChanged();
1520            addToolBar(TOP_GROUP,SEARCH_BAR_LAYER,searchBar);
1521        }
1522    } //}}}
1523
1524    //{{{ createEditPane() method
1525    private EditPane createEditPane(Buffer buffer)
1526    {
1527        EditPane editPane = new EditPane(this,buffer);
1528        JEditTextArea textArea = editPane.getTextArea();
1529        textArea.addFocusListener(new FocusHandler());
1530        textArea.addCaretListener(new CaretHandler());
1531        textArea.addScrollListener(new ScrollHandler());
1532        EditBus.send(new EditPaneUpdate(editPane,EditPaneUpdate.CREATED));
1533        return editPane;
1534    } //}}}
1535
1536    //{{{ setEditPane() method
1537    private void setEditPane(EditPane editPane)
1538    {
1539        this.editPane = editPane;
1540        status.updateCaretStatus();
1541        status.updateBufferStatus();
1542        status.updateMiscStatus();
1543
1544        // repaint the gutter so that the border color
1545        // reflects the focus state
1546        updateGutterBorders();
1547
1548        EditBus.send(new ViewUpdate(this,ViewUpdate.EDIT_PANE_CHANGED));
1549    } //}}}
1550
1551    //{{{ handleBufferUpdate() method
1552    private void handleBufferUpdate(BufferUpdate msg)
1553    {
1554        Buffer buffer = msg.getBuffer();
1555        if(msg.getWhat() == BufferUpdate.DIRTY_CHANGED
1556            || msg.getWhat() == BufferUpdate.LOADED)
1557        {
1558            EditPane[] editPanes = getEditPanes();
1559            for(int i = 0; i < editPanes.length; i++)
1560            {
1561                if(editPanes[i].getBuffer() == buffer)
1562                {
1563                    updateTitle();
1564                    break;
1565                }
1566            }
1567        }
1568    } //}}}
1569
1570    //{{{ handleEditPaneUpdate() method
1571    private void handleEditPaneUpdate(EditPaneUpdate msg)
1572    {
1573        EditPane editPane = msg.getEditPane();
1574        if(editPane.getView() == this
1575            && msg.getWhat() == EditPaneUpdate.BUFFER_CHANGED
1576            && editPane.getBuffer().isLoaded())
1577        {
1578            status.updateCaretStatus();
1579            status.updateBufferStatus();
1580            status.updateMiscStatus();
1581        }
1582    } //}}}
1583
1584    //{{{ updateGutterBorders() method
1585    /**
1586     * Updates the borders of all gutters in this view to reflect the
1587     * currently focused text area.
1588     * @since jEdit 2.6final
1589     */
1590    private void updateGutterBorders()
1591    {
1592        EditPane[] editPanes = getEditPanes();
1593        for(int i = 0; i < editPanes.length; i++)
1594            editPanes[i].getTextArea().getGutter().updateBorder();
1595    } //}}}
1596
1597    //}}}
1598
1599    //{{{ Inner classes
1600
1601    //{{{ CaretHandler class
1602    class CaretHandler implements CaretListener
1603    {
1604        public void caretUpdate(CaretEvent evt)
1605        {
1606            if(evt.getSource() == getTextArea())
1607                status.updateCaretStatus();
1608        }
1609    } //}}}
1610
1611    //{{{ FocusHandler class
1612    class FocusHandler extends FocusAdapter
1613    {
1614        public void focusGained(FocusEvent evt)
1615        {
1616            // walk up hierarchy, looking for an EditPane
1617            Component comp = (Component)evt.getSource();
1618            while(!(comp instanceof EditPane))
1619            {
1620                if(comp == null)
1621                    return;
1622
1623                comp = comp.getParent();
1624            }
1625
1626            if(comp != editPane)
1627                setEditPane((EditPane)comp);
1628            else
1629                updateGutterBorders();
1630        }
1631    } //}}}
1632
1633    //{{{ ScrollHandler class
1634    class ScrollHandler implements ScrollListener
1635    {
1636        public void scrolledVertically(TextArea textArea)
1637        {
1638            if(getTextArea() == textArea)
1639                status.updateCaretStatus();
1640        }
1641
1642        public void scrolledHorizontally(TextArea textArea) {}
1643    } //}}}
1644
1645    //{{{ WindowHandler class
1646    class WindowHandler extends WindowAdapter
1647    {
1648        public void windowActivated(WindowEvent evt)
1649        {
1650            boolean editPaneChanged =
1651                jEdit.getActiveView() != View.this;
1652            jEdit.setActiveView(View.this);
1653
1654            // People have reported hangs with JDK 1.4; might be
1655            // caused by modal dialogs being displayed from
1656            // windowActivated()
1657            SwingUtilities.invokeLater(new Runnable  ()
1658            {
1659                public void run()
1660                {
1661                    jEdit.checkBufferStatus(View.this);
1662                }
1663            });
1664
1665            if (editPaneChanged)
1666            {
1667                EditBus.send(new ViewUpdate(View.this,ViewUpdate
1668                    .ACTIVATED));
1669            }
1670        }
1671
1672        public void windowClosing(WindowEvent evt)
1673        {
1674            jEdit.closeView(View.this);
1675        }
1676    } //}}}
1677
1678    //{{{ ViewConfig class
1679    public static class ViewConfig
1680    {
1681        public boolean plainView;
1682        public String   splitConfig;
1683        public int x, y, width, height, extState;
1684
1685        // dockables
1686        public String   top, left, bottom, right;
1687        public int topPos, leftPos, bottomPos, rightPos;
1688
1689        public ViewConfig()
1690        {
1691        }
1692
1693        public ViewConfig(boolean plainView)
1694        {
1695            this.plainView = plainView;
1696            String   prefix = plainView ? "plain-view" : "view";
1697            x = jEdit.getIntegerProperty(prefix + ".x",0);
1698            y = jEdit.getIntegerProperty(prefix + ".y",0);
1699            width = jEdit.getIntegerProperty(prefix + ".width",0);
1700            height = jEdit.getIntegerProperty(prefix + ".height",0);
1701            extState = jEdit.getIntegerProperty(prefix + ".extendedState",NORMAL);
1702        }
1703
1704        public ViewConfig(boolean plainView, String   splitConfig,
1705            int x, int y, int width, int height, int extState)
1706        {
1707            this.plainView = plainView;
1708            this.splitConfig = splitConfig;
1709            this.x = x;
1710            this.y = y;
1711            this.width = width;
1712            this.height = height;
1713            this.extState = extState;
1714        }
1715    } //}}}
1716
1717    //{{{ MyFocusTraversalPolicy class
1718    static class MyFocusTraversalPolicy extends LayoutFocusTraversalPolicy
1719    {
1720        public Component getDefaultComponent(Container focusCycleRoot)
1721        {
1722            return GUIUtilities.getView(focusCycleRoot).getTextArea();
1723        }
1724    } //}}}
1725
1726    //}}}
1727}
1728
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags