0001: /*
0002: * EditPane.java - Text area and buffer switcher
0003: * :tabSize=8:indentSize=8:noTabs=false:
0004: * :folding=explicit:collapseFolds=1:
0005: *
0006: * Copyright (C) 2000, 2005 Slava Pestov
0007: *
0008: * This program is free software; you can redistribute it and/or
0009: * modify it under the terms of the GNU General Public License
0010: * as published by the Free Software Foundation; either version 2
0011: * of the License, or any later version.
0012: *
0013: * This program is distributed in the hope that it will be useful,
0014: * but WITHOUT ANY WARRANTY; without even the implied warranty of
0015: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0016: * GNU General Public License for more details.
0017: *
0018: * You should have received a copy of the GNU General Public License
0019: * along with this program; if not, write to the Free Software
0020: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
0021: */
0022:
0023: package org.gjt.sp.jedit;
0024:
0025: //{{{ Imports
0026: import javax.swing.*;
0027: import java.awt.event.*;
0028: import java.awt.*;
0029: import java.util.HashMap;
0030: import java.util.Map;
0031:
0032: import org.gjt.sp.jedit.gui.*;
0033: import org.gjt.sp.jedit.io.VFSManager;
0034: import org.gjt.sp.jedit.msg.*;
0035: import org.gjt.sp.jedit.options.GlobalOptions;
0036: import org.gjt.sp.jedit.syntax.SyntaxStyle;
0037: import org.gjt.sp.jedit.textarea.*;
0038: import org.gjt.sp.jedit.buffer.JEditBuffer;
0039:
0040: //}}}
0041:
0042: /**
0043: * A panel containing a text area.<p>
0044: *
0045: * In a BeanShell script, you can obtain the current edit pane from the
0046: * <code>editPane</code> variable.<p>
0047: *
0048: *
0049: * Each View can have multiple editPanes, one is active at a time.
0050: * Each EditPane has a single JEditTextArea, and is operating on single buffer.
0051: * The EditPane also can switch buffers.
0052: *
0053: * This is the "controller" between a JEditTextArea (view) and a buffer (model).
0054: *
0055: * This class does not have a public constructor.
0056: * Edit panes can be created and destroyed using methods in the
0057: * {@link View} class.<p>
0058: *
0059: *
0060: * @see View#splitHorizontally()
0061: * @see View#splitVertically()
0062: * @see View#unsplitCurrent()
0063: * @see View#unsplit()
0064: * @see View#getEditPane()
0065: * @see View#getEditPanes()
0066: *
0067: * @author Slava Pestov
0068: * @version $Id: EditPane.java 10993 2007-11-07 21:13:44Z kpouer $
0069: */
0070: public class EditPane extends JPanel implements EBComponent {
0071: //{{{ getView() method
0072: /**
0073: * Returns the view containing this edit pane.
0074: * @since jEdit 2.5pre2
0075: */
0076: public View getView() {
0077: return view;
0078: } //}}}
0079:
0080: //{{{ getBuffer() method
0081: /**
0082: * Returns the current buffer.
0083: * @since jEdit 2.5pre2
0084: */
0085: public Buffer getBuffer() {
0086: return buffer;
0087: } //}}}
0088:
0089: //{{{ setBuffer() method
0090: /**
0091: * Sets the current buffer.
0092: * @param buffer The buffer to edit.
0093: * @since jEdit 2.5pre2
0094: */
0095: public void setBuffer(Buffer buffer) {
0096: setBuffer(buffer, true);
0097: } //}}}
0098:
0099: //{{{ setBuffer() method
0100: /**
0101: * Sets the current buffer.
0102: * @param buffer The buffer to edit.
0103: * @param requestFocus true if the textarea should request focus, false otherwise
0104: * @since jEdit 4.3pre6
0105: */
0106: public void setBuffer(final Buffer buffer, boolean requestFocus) {
0107:
0108: if (buffer == null)
0109: throw new NullPointerException();
0110:
0111: if (this .buffer == buffer)
0112: return;
0113:
0114: //if(buffer.insideCompoundEdit())
0115: // buffer.endCompoundEdit();
0116: EditBus.send(new BufferChanging(this , buffer));
0117: recentBuffer = this .buffer;
0118: if (recentBuffer != null)
0119: saveCaretInfo();
0120: this .buffer = buffer;
0121:
0122: textArea.setBuffer(buffer);
0123:
0124: if (!init) {
0125: view.updateTitle();
0126:
0127: if (bufferSwitcher != null) {
0128: if (bufferSwitcher.getSelectedItem() != buffer)
0129: bufferSwitcher.setSelectedItem(buffer);
0130: bufferSwitcher.setToolTipText(buffer.getPath());
0131: }
0132:
0133: EditBus.send(new EditPaneUpdate(this ,
0134: EditPaneUpdate.BUFFER_CHANGED));
0135: }
0136:
0137: if (requestFocus) {
0138: SwingUtilities.invokeLater(new Runnable() {
0139: public void run() {
0140: // only do this if we are the current edit pane
0141: if (view.getEditPane() == EditPane.this
0142: && (bufferSwitcher == null || !bufferSwitcher
0143: .isPopupVisible())) {
0144: textArea.requestFocus();
0145: }
0146: }
0147: });
0148: }
0149:
0150: // Only do this after all I/O requests are complete
0151: Runnable runnable = new Runnable() {
0152: public void run() {
0153: // avoid a race condition
0154: // see bug #834338
0155: if (buffer == getBuffer())
0156: loadCaretInfo();
0157: }
0158: };
0159:
0160: if (buffer.isPerformingIO())
0161: VFSManager.runInAWTThread(runnable);
0162: else
0163: runnable.run();
0164: } //}}}
0165:
0166: //{{{ prevBuffer() method
0167: /**
0168: * Selects the previous buffer.
0169: * @since jEdit 2.7pre2
0170: */
0171: public void prevBuffer() {
0172: Buffer buffer = this .buffer.getPrev();
0173: if (buffer == null)
0174: setBuffer(jEdit.getLastBuffer());
0175: else
0176: setBuffer(buffer);
0177: } //}}}
0178:
0179: //{{{ nextBuffer() method
0180: /**
0181: * Selects the next buffer.
0182: * @since jEdit 2.7pre2
0183: */
0184: public void nextBuffer() {
0185: Buffer buffer = this .buffer.getNext();
0186: if (buffer == null)
0187: setBuffer(jEdit.getFirstBuffer());
0188: else
0189: setBuffer(buffer);
0190: } //}}}
0191:
0192: //{{{ recentBuffer() method
0193: /**
0194: * Selects the most recently edited buffer.
0195: * @since jEdit 2.7pre2
0196: */
0197: public void recentBuffer() {
0198: if (recentBuffer != null)
0199: setBuffer(recentBuffer);
0200: else
0201: getToolkit().beep();
0202: } //}}}
0203:
0204: //{{{ focusOnTextArea() method
0205: /**
0206: * Sets the focus onto the text area.
0207: * @since jEdit 2.5pre2
0208: */
0209: public void focusOnTextArea() {
0210: SwingUtilities.invokeLater(new Runnable() {
0211: public void run() {
0212: textArea.requestFocus();
0213: }
0214: });
0215: } //}}}
0216:
0217: //{{{ getTextArea() method
0218: /**
0219: * Returns the view's text area.
0220: * @since jEdit 2.5pre2
0221: */
0222: public JEditTextArea getTextArea() {
0223: return textArea;
0224: } //}}}
0225:
0226: //{{{ getBufferSwitcher() method
0227: /**
0228: * Returns the buffer switcher combo box instance.
0229: * @since jEdit 4.1pre8
0230: */
0231: public BufferSwitcher getBufferSwitcher() {
0232: return bufferSwitcher;
0233: } //}}}
0234:
0235: //{{{ showBufferSwitcher() method
0236: /**
0237: * Shows the buffer switcher combo box.
0238: * @since jEdit 4.1pre8
0239: */
0240: public void showBufferSwitcher() {
0241: if (bufferSwitcher == null)
0242: getToolkit().beep();
0243: else {
0244: bufferSwitcher.requestFocus();
0245: bufferSwitcher.showPopup();
0246: }
0247: } //}}}
0248:
0249: //{{{ saveCaretInfo() method
0250: /**
0251: * Saves the caret information to the current buffer.
0252: * @since jEdit 2.5pre2
0253: */
0254: public void saveCaretInfo() {
0255: if (!buffer.isLoaded())
0256: return;
0257:
0258: buffer.setIntegerProperty(Buffer.CARET, textArea
0259: .getCaretPosition());
0260:
0261: // save a map of buffer.getPath() -> CaretInfo, this is necessary for
0262: // when the same buffer is open in more than one EditPane and the user
0263: // is switching between buffers. We want to keep the caret in the
0264: // right position in each EditPane, which won't be the case if we
0265: // just use the buffer caret property.
0266: Map<String, CaretInfo> carets = (Map<String, CaretInfo>) getClientProperty(CARETS);
0267: if (carets == null) {
0268: carets = new HashMap<String, CaretInfo>();
0269: putClientProperty(CARETS, carets);
0270: }
0271: CaretInfo caretInfo = carets.get(buffer.getPath());
0272: if (caretInfo == null) {
0273: caretInfo = new CaretInfo();
0274: carets.put(buffer.getPath(), caretInfo);
0275: }
0276: caretInfo.caret = textArea.getCaretPosition();
0277:
0278: Selection[] selection = textArea.getSelection();
0279: for (int i = 0; i < selection.length; i++)
0280: selection[i] = (Selection) selection[i].clone();
0281: buffer.setProperty(Buffer.SELECTION, selection);
0282: caretInfo.selection = selection;
0283:
0284: caretInfo.rectangularSelection = textArea
0285: .isRectangularSelectionEnabled();
0286: caretInfo.multipleSelection = textArea
0287: .isMultipleSelectionEnabled();
0288:
0289: buffer.setIntegerProperty(Buffer.SCROLL_VERT, textArea
0290: .getFirstPhysicalLine());
0291: caretInfo.scrollVert = textArea.getFirstPhysicalLine();
0292: buffer.setIntegerProperty(Buffer.SCROLL_HORIZ, textArea
0293: .getHorizontalOffset());
0294: caretInfo.scrollHoriz = textArea.getHorizontalOffset();
0295: if (!buffer.isUntitled()) {
0296: BufferHistory.setEntry(buffer.getPath(), textArea
0297: .getCaretPosition(), (Selection[]) buffer
0298: .getProperty(Buffer.SELECTION), buffer
0299: .getStringProperty(JEditBuffer.ENCODING), buffer
0300: .getMode().getName());
0301: }
0302: } //}}}
0303:
0304: //{{{ loadCaretInfo() method
0305: /**
0306: * Loads the caret and selection information from this EditPane, fall
0307: * back to the information from the current buffer if none is already
0308: * in this EditPane.
0309: * @since jEdit 2.5pre2
0310: */
0311: public void loadCaretInfo() {
0312: // get our internal map of buffer -> CaretInfo since there might
0313: // be current info already
0314: Map<String, CaretInfo> carets = (Map<String, CaretInfo>) getClientProperty(CARETS);
0315: if (carets == null) {
0316: carets = new HashMap<String, CaretInfo>();
0317: putClientProperty(CARETS, carets);
0318: }
0319: CaretInfo caretInfo = carets.get(buffer.getPath());
0320: if (caretInfo == null) {
0321: caretInfo = new CaretInfo();
0322: }
0323:
0324: // set the position of the caret itself.
0325: // Caret position could be stored in the internal map already,
0326: // if so, use that one first. Otherwise, fall back to any
0327: // previously saved caret position that was stored in the
0328: // buffer properties.
0329: int caret = caretInfo.caret;
0330: if (caret == -1
0331: || buffer.getBooleanProperty(Buffer.CARET_POSITIONED)) {
0332: Integer i = (Integer) buffer.getProperty(Buffer.CARET);
0333: caret = i == null ? -1 : i;
0334: }
0335: buffer.unsetProperty(Buffer.CARET_POSITIONED);
0336:
0337: if (caret != -1)
0338: textArea.setCaretPosition(Math.min(caret, buffer
0339: .getLength()));
0340:
0341: // set any selections
0342: Selection[] selection = caretInfo.selection;
0343: if (selection == null) {
0344: selection = (Selection[]) buffer
0345: .getProperty(Buffer.SELECTION);
0346: }
0347: if (selection != null) {
0348: for (int i = 0; i < selection.length; i++) {
0349: Selection s = selection[i];
0350: int max = buffer.getLength();
0351: if (s.getStart() > max || s.getEnd() > max)
0352: selection[i] = null;
0353: }
0354: }
0355: textArea.setSelection(selection);
0356: textArea
0357: .setRectangularSelectionEnabled(caretInfo.rectangularSelection);
0358: textArea
0359: .setMultipleSelectionEnabled(caretInfo.multipleSelection);
0360: // set firstLine value
0361: int firstLine = caretInfo.scrollVert;
0362: if (firstLine == -1) {
0363: Integer i = (Integer) buffer
0364: .getProperty(Buffer.SCROLL_VERT);
0365: firstLine = i == null ? -1 : i;
0366: }
0367:
0368: if (firstLine != -1)
0369: textArea.setFirstPhysicalLine(firstLine);
0370:
0371: // set horizontal offset
0372: int horizontalOffset = caretInfo.scrollHoriz;
0373: if (horizontalOffset == -1) {
0374: Integer i = (Integer) buffer
0375: .getProperty(Buffer.SCROLL_HORIZ);
0376: horizontalOffset = i == null ? -1 : i;
0377: }
0378:
0379: if (horizontalOffset != -1)
0380: textArea.setHorizontalOffset(horizontalOffset);
0381:
0382: /* Silly bug workaround #8694. If you look at the above code,
0383: * note that we restore the saved caret position first, then
0384: * scroll to the saved location. However, the caret changing
0385: * can itself result in scrolling to a different location than
0386: * what was saved; and since moveCaretPosition() calls
0387: * updateBracketHighlight(), the bracket highlight's out of
0388: * bounds calculation will rely on a different set of physical
0389: * first/last lines than what we will end up with eventually.
0390: * Instead of confusing the user with status messages that
0391: * appear at random when switching buffers, we simply hide the
0392: * message altogether. */
0393: view.getStatus().setMessage(null);
0394: } //}}}
0395:
0396: //{{{ bufferRenamed() method
0397: /**
0398: * This method should be called by the Buffer when the path is changing.
0399: * @param oldPath the old path of the buffer
0400: * @param newPath the new path of the buffer
0401: */
0402: void bufferRenamed(String oldPath, String newPath) {
0403: Map<String, CaretInfo> carets = (Map<String, CaretInfo>) getClientProperty(CARETS);
0404: if (carets == null)
0405: return;
0406: CaretInfo caretInfo = carets.remove(oldPath);
0407: if (caretInfo != null)
0408: carets.put(newPath, caretInfo);
0409:
0410: } //}}}
0411:
0412: //{{{
0413: /**
0414: * Need to track this info for each buffer that this EditPane might edit
0415: * since a buffer may be open in more than one EditPane at a time. That
0416: * means we need to track this info at the EditPane level rather than
0417: * the buffer level.
0418: */
0419: private static class CaretInfo {
0420: public int caret = -1;
0421: public Selection[] selection;
0422: public int scrollVert = -1;
0423: public int scrollHoriz = -1;
0424: public boolean rectangularSelection;
0425: public boolean multipleSelection;
0426: } //}}}
0427:
0428: //{{{ goToNextMarker() method
0429: /**
0430: * Moves the caret to the next marker.
0431: * @since jEdit 4.3pre3
0432: */
0433: public void goToNextMarker(boolean select) {
0434: java.util.List<Marker> markers = buffer.getMarkers();
0435: if (markers.isEmpty()) {
0436: getToolkit().beep();
0437: return;
0438: }
0439:
0440: Marker marker = null;
0441:
0442: int caret = textArea.getCaretPosition();
0443:
0444: for (int i = 0; i < markers.size(); i++) {
0445: Marker _marker = markers.get(i);
0446: if (_marker.getPosition() > caret) {
0447: marker = _marker;
0448: break;
0449: }
0450: }
0451: // the markers list is not empty at this point
0452: if (marker == null)
0453: marker = markers.get(0);
0454:
0455: if (select)
0456: textArea.extendSelection(caret, marker.getPosition());
0457: else if (!textArea.isMultipleSelectionEnabled())
0458: textArea.selectNone();
0459: textArea.moveCaretPosition(marker.getPosition());
0460: } //}}}
0461:
0462: //{{{ goToPrevMarker() method
0463: /**
0464: * Moves the caret to the previous marker.
0465: * @since jEdit 2.7pre2
0466: */
0467: public void goToPrevMarker(boolean select) {
0468: java.util.List<Marker> markers = buffer.getMarkers();
0469: if (markers.isEmpty()) {
0470: getToolkit().beep();
0471: return;
0472: }
0473:
0474: int caret = textArea.getCaretPosition();
0475:
0476: Marker marker = null;
0477: for (int i = markers.size() - 1; i >= 0; i--) {
0478: Marker _marker = markers.get(i);
0479: if (_marker.getPosition() < caret) {
0480: marker = _marker;
0481: break;
0482: }
0483: }
0484:
0485: if (marker == null)
0486: marker = markers.get(markers.size() - 1);
0487:
0488: if (select)
0489: textArea.extendSelection(caret, marker.getPosition());
0490: else if (!textArea.isMultipleSelectionEnabled())
0491: textArea.selectNone();
0492: textArea.moveCaretPosition(marker.getPosition());
0493: } //}}}
0494:
0495: //{{{ goToMarker() method
0496: /**
0497: * Moves the caret to the marker with the specified shortcut.
0498: * @param shortcut The shortcut
0499: * @param select True if the selection should be extended,
0500: * false otherwise
0501: * @since jEdit 3.2pre2
0502: */
0503: public void goToMarker(char shortcut, boolean select) {
0504: Marker marker = buffer.getMarker(shortcut);
0505: if (marker == null) {
0506: getToolkit().beep();
0507: return;
0508: }
0509:
0510: int pos = marker.getPosition();
0511:
0512: if (select)
0513: textArea.extendSelection(textArea.getCaretPosition(), pos);
0514: else if (!textArea.isMultipleSelectionEnabled())
0515: textArea.selectNone();
0516: textArea.moveCaretPosition(pos);
0517: } //}}}
0518:
0519: //{{{ addMarker() method
0520: /**
0521: * Adds a marker at the caret position.
0522: * @since jEdit 3.2pre1
0523: */
0524: public void addMarker() {
0525: int caretLine = textArea.getCaretLine();
0526:
0527: // always add markers on selected lines
0528: Selection[] selection = textArea.getSelection();
0529: for (int i = 0; i < selection.length; i++) {
0530: Selection s = selection[i];
0531: if (s.getStartLine() != s.getEndLine()) {
0532: if (s.getStartLine() != caretLine)
0533: buffer.addMarker('\0', s.getStart());
0534: }
0535:
0536: if (s.getEndLine() != caretLine)
0537: buffer.addMarker('\0', s.getEnd());
0538: }
0539:
0540: // toggle marker on caret line
0541: buffer.addOrRemoveMarker('\0', textArea.getCaretPosition());
0542: } //}}}
0543:
0544: //{{{ swapMarkerAndCaret() method
0545: /**
0546: * Moves the caret to the marker with the specified shortcut,
0547: * then sets the marker position to the former caret position.
0548: * @param shortcut The shortcut
0549: * @since jEdit 3.2pre2
0550: */
0551: public void swapMarkerAndCaret(char shortcut) {
0552: Marker marker = buffer.getMarker(shortcut);
0553: if (marker == null) {
0554: getToolkit().beep();
0555: return;
0556: }
0557:
0558: int caret = textArea.getCaretPosition();
0559:
0560: textArea.setCaretPosition(marker.getPosition());
0561: buffer.addMarker(shortcut, caret);
0562: } //}}}
0563:
0564: //{{{ handleMessage() method
0565: public void handleMessage(EBMessage msg) {
0566: if (msg instanceof PropertiesChanged) {
0567: propertiesChanged();
0568: loadBufferSwitcher();
0569: } else if (msg instanceof BufferUpdate)
0570: handleBufferUpdate((BufferUpdate) msg);
0571: } //}}}
0572:
0573: //{{{ getMinimumSize() method
0574: /**
0575: * Returns 0,0 for split pane compatibility.
0576: */
0577: public final Dimension getMinimumSize() {
0578: return new Dimension(0, 0);
0579: } //}}}
0580:
0581: //{{{ toString() method
0582: public String toString() {
0583: return getClass().getName() + '['
0584: + (view.getEditPane() == this ? "active" : "inactive")
0585: + ']';
0586: } //}}}
0587:
0588: //{{{ Package-private members
0589:
0590: //{{{ EditPane constructor
0591: EditPane(View view, Buffer buffer) {
0592: super (new BorderLayout());
0593:
0594: init = true;
0595:
0596: this .view = view;
0597:
0598: EditBus.addToBus(this );
0599:
0600: textArea = new JEditTextArea(view);
0601: textArea.getPainter().setAntiAlias(
0602: new AntiAlias(jEdit.getProperty("view.antiAlias")));
0603: textArea.setMouseHandler(new MouseHandler(textArea));
0604: textArea.setTransferHandler(new TextAreaTransferHandler());
0605: markerHighlight = new MarkerHighlight();
0606: textArea.getGutter().addExtension(markerHighlight);
0607: textArea.addStatusListener(new StatusHandler());
0608:
0609: add(BorderLayout.CENTER, textArea);
0610:
0611: propertiesChanged();
0612:
0613: if (buffer == null)
0614: setBuffer(jEdit.getFirstBuffer());
0615: else
0616: setBuffer(buffer);
0617:
0618: loadBufferSwitcher();
0619:
0620: init = false;
0621: } //}}}
0622:
0623: //{{{ close() method
0624: void close() {
0625: saveCaretInfo();
0626: EditBus
0627: .send(new EditPaneUpdate(this , EditPaneUpdate.DESTROYED));
0628: EditBus.removeFromBus(this );
0629: textArea.dispose();
0630: } //}}}
0631:
0632: //}}}
0633:
0634: //{{{ Private members
0635:
0636: //{{{ Instance variables
0637: private boolean init;
0638: /** The View where the edit pane is. */
0639: private final View view;
0640: /** The current buffer. */
0641: private Buffer buffer;
0642: private Buffer recentBuffer;
0643: private BufferSwitcher bufferSwitcher;
0644: /** The textArea inside the edit pane. */
0645: private final JEditTextArea textArea;
0646: private final MarkerHighlight markerHighlight;
0647:
0648: private static final String CARETS = "Buffer->caret";
0649:
0650: //}}}
0651:
0652: //{{{ propertiesChanged() method
0653: private void propertiesChanged() {
0654: TextAreaPainter painter = textArea.getPainter();
0655:
0656: initPainter(painter);
0657: Gutter gutter = textArea.getGutter();
0658: gutter.setExpanded(jEdit
0659: .getBooleanProperty("view.gutter.lineNumbers"));
0660: int interval = jEdit.getIntegerProperty(
0661: "view.gutter.highlightInterval", 5);
0662: gutter.setHighlightInterval(interval);
0663: gutter
0664: .setCurrentLineHighlightEnabled(jEdit
0665: .getBooleanProperty("view.gutter.highlightCurrentLine"));
0666: gutter.setStructureHighlightEnabled(jEdit
0667: .getBooleanProperty("view.gutter.structureHighlight"));
0668: gutter
0669: .setStructureHighlightColor(jEdit
0670: .getColorProperty("view.gutter.structureHighlightColor"));
0671: gutter.setBackground(jEdit
0672: .getColorProperty("view.gutter.bgColor"));
0673: gutter.setForeground(jEdit
0674: .getColorProperty("view.gutter.fgColor"));
0675: gutter.setHighlightedForeground(jEdit
0676: .getColorProperty("view.gutter.highlightColor"));
0677: gutter.setFoldColor(jEdit
0678: .getColorProperty("view.gutter.foldColor"));
0679: markerHighlight.setMarkerHighlightColor(jEdit
0680: .getColorProperty("view.gutter.markerColor"));
0681: markerHighlight.setMarkerHighlightEnabled(jEdit
0682: .getBooleanProperty("view.gutter.markerHighlight"));
0683: gutter.setCurrentLineForeground(jEdit
0684: .getColorProperty("view.gutter.currentLineColor"));
0685: String alignment = jEdit
0686: .getProperty("view.gutter.numberAlignment");
0687: if ("right".equals(alignment)) {
0688: gutter.setLineNumberAlignment(Gutter.RIGHT);
0689: } else if ("center".equals(alignment)) {
0690: gutter.setLineNumberAlignment(Gutter.CENTER);
0691: } else // left == default case
0692: {
0693: gutter.setLineNumberAlignment(Gutter.LEFT);
0694: }
0695:
0696: gutter.setFont(jEdit.getFontProperty("view.gutter.font"));
0697:
0698: int width = jEdit.getIntegerProperty("view.gutter.borderWidth",
0699: 3);
0700: gutter
0701: .setBorder(
0702: width,
0703: jEdit
0704: .getColorProperty("view.gutter.focusBorderColor"),
0705: jEdit
0706: .getColorProperty("view.gutter.noFocusBorderColor"),
0707: textArea.getPainter().getBackground());
0708:
0709: textArea.setCaretBlinkEnabled(jEdit
0710: .getBooleanProperty("view.caretBlink"));
0711:
0712: textArea.setElectricScroll(jEdit.getIntegerProperty(
0713: "view.electricBorders", 0));
0714:
0715: // Set up the right-click popup menu
0716: JPopupMenu popup = GUIUtilities.loadPopupMenu("view.context");
0717: JMenuItem customize = new JMenuItem(jEdit
0718: .getProperty("view.context.customize"));
0719: customize.addActionListener(new ActionListener() {
0720: public void actionPerformed(ActionEvent evt) {
0721: new GlobalOptions(view, "context");
0722: }
0723: });
0724: popup.addSeparator();
0725: popup.add(customize);
0726: textArea.setRightClickPopup(popup);
0727:
0728: // use old property name for backwards compatibility
0729: textArea.setQuickCopyEnabled(jEdit
0730: .getBooleanProperty("view.middleMousePaste"));
0731:
0732: textArea.setDragEnabled(jEdit
0733: .getBooleanProperty("view.dragAndDrop"));
0734:
0735: textArea.setJoinNonWordChars(jEdit
0736: .getBooleanProperty("view.joinNonWordChars"));
0737:
0738: textArea
0739: .setCtrlForRectangularSelection(jEdit
0740: .getBooleanProperty("view.ctrlForRectangularSelection"));
0741:
0742: textArea.propertiesChanged();
0743:
0744: if (bufferSwitcher != null) {
0745: bufferSwitcher.setMaximumRowCount(jEdit.getIntegerProperty(
0746: "bufferSwitcher.maxRowCount", 10));
0747: }
0748: } //}}}
0749:
0750: //{{{ propertiesChanged() method
0751: /**
0752: * Init the painter of a textarea.
0753: *
0754: * @param painter the painter of a textarea
0755: * @since jEdit 4.3pre12
0756: */
0757: public static void initPainter(TextAreaPainter painter) {
0758: painter.setFont(jEdit.getFontProperty("view.font"));
0759: painter.setStructureHighlightEnabled(jEdit
0760: .getBooleanProperty("view.structureHighlight"));
0761: painter.setStructureHighlightColor(jEdit
0762: .getColorProperty("view.structureHighlightColor"));
0763: painter.setEOLMarkersPainted(jEdit
0764: .getBooleanProperty("view.eolMarkers"));
0765: painter.setEOLMarkerColor(jEdit
0766: .getColorProperty("view.eolMarkerColor"));
0767: painter.setWrapGuidePainted(jEdit
0768: .getBooleanProperty("view.wrapGuide"));
0769: painter.setWrapGuideColor(jEdit
0770: .getColorProperty("view.wrapGuideColor"));
0771: painter
0772: .setCaretColor(jEdit
0773: .getColorProperty("view.caretColor"));
0774: painter.setSelectionColor(jEdit
0775: .getColorProperty("view.selectionColor"));
0776: painter.setMultipleSelectionColor(jEdit
0777: .getColorProperty("view.multipleSelectionColor"));
0778: painter.setBackground(jEdit.getColorProperty("view.bgColor"));
0779: painter.setForeground(jEdit.getColorProperty("view.fgColor"));
0780: painter.setBlockCaretEnabled(jEdit
0781: .getBooleanProperty("view.blockCaret"));
0782: painter.setLineHighlightEnabled(jEdit
0783: .getBooleanProperty("view.lineHighlight"));
0784: painter.setLineHighlightColor(jEdit
0785: .getColorProperty("view.lineHighlightColor"));
0786: painter.setAntiAlias(new AntiAlias(jEdit
0787: .getProperty("view.antiAlias")));
0788: painter.setFractionalFontMetricsEnabled(jEdit
0789: .getBooleanProperty("view.fracFontMetrics"));
0790:
0791: String defaultFont = jEdit.getProperty("view.font");
0792: int defaultFontSize = jEdit.getIntegerProperty("view.fontsize",
0793: 12);
0794: painter.setStyles(GUIUtilities.loadStyles(defaultFont,
0795: defaultFontSize));
0796:
0797: SyntaxStyle[] foldLineStyle = new SyntaxStyle[4];
0798: for (int i = 0; i <= 3; i++) {
0799: foldLineStyle[i] = GUIUtilities.parseStyle(jEdit
0800: .getProperty("view.style.foldLine." + i),
0801: defaultFont, defaultFontSize);
0802: }
0803: painter.setFoldLineStyle(foldLineStyle);
0804: } //}}}
0805:
0806: //{{{ loadBufferSwitcher() method
0807: private void loadBufferSwitcher() {
0808: if (jEdit.getBooleanProperty("view.showBufferSwitcher")) {
0809: if (bufferSwitcher == null) {
0810: bufferSwitcher = new BufferSwitcher(this );
0811: add(BorderLayout.NORTH, bufferSwitcher);
0812: bufferSwitcher.updateBufferList();
0813: revalidate();
0814: }
0815: } else if (bufferSwitcher != null) {
0816: remove(bufferSwitcher);
0817: revalidate();
0818: bufferSwitcher = null;
0819: }
0820: } //}}}
0821:
0822: //{{{ handleBufferUpdate() method
0823: private void handleBufferUpdate(BufferUpdate msg) {
0824: Buffer _buffer = msg.getBuffer();
0825: if (msg.getWhat() == BufferUpdate.CREATED) {
0826: if (bufferSwitcher != null)
0827: bufferSwitcher.updateBufferList();
0828:
0829: /* When closing the last buffer, the BufferUpdate.CLOSED
0830: * handler doesn't call setBuffer(), because null buffers
0831: * are not supported. Instead, it waits for the subsequent
0832: * 'Untitled' file creation. */
0833: if (buffer.isClosed()) {
0834: setBuffer(jEdit.getFirstBuffer(), msg.getView() == view);
0835: // since recentBuffer will be set to the one that
0836: // was closed
0837: recentBuffer = null;
0838: }
0839: } else if (msg.getWhat() == BufferUpdate.CLOSED) {
0840: if (bufferSwitcher != null)
0841: bufferSwitcher.updateBufferList();
0842:
0843: if (_buffer == buffer) {
0844: // The closed buffer is the current buffer
0845: Buffer newBuffer = recentBuffer != null ? recentBuffer
0846: : _buffer.getPrev();
0847:
0848: if (newBuffer != null && !newBuffer.isClosed()) {
0849: setBuffer(newBuffer);
0850: recentBuffer = newBuffer.getPrev();
0851: } else if (jEdit.getBufferCount() != 0) {
0852: setBuffer(jEdit.getFirstBuffer());
0853: recentBuffer = null;
0854: }
0855: } else if (_buffer == recentBuffer)
0856: recentBuffer = null;
0857:
0858: Buffer closedBuffer = msg.getBuffer();
0859: if (closedBuffer.isUntitled()) {
0860: // the buffer was a new file so I do not need to keep it's informations
0861: Map<String, CaretInfo> carets = (Map<String, CaretInfo>) getClientProperty(CARETS);
0862: if (carets != null)
0863: carets.remove(closedBuffer.getPath());
0864: }
0865: } else if (msg.getWhat() == BufferUpdate.LOAD_STARTED) {
0866: if (_buffer == buffer) {
0867: textArea.setCaretPosition(0);
0868: textArea.getPainter().repaint();
0869: }
0870: } else if (msg.getWhat() == BufferUpdate.LOADED) {
0871: if (_buffer == buffer) {
0872: textArea.repaint();
0873: if (bufferSwitcher != null)
0874: bufferSwitcher.updateBufferList();
0875:
0876: if (view.getEditPane() == this ) {
0877: StatusBar status = view.getStatus();
0878: status.updateCaretStatus();
0879: status.updateBufferStatus();
0880: status.updateMiscStatus();
0881: }
0882:
0883: loadCaretInfo();
0884: }
0885:
0886: } else if (msg.getWhat() == BufferUpdate.DIRTY_CHANGED) {
0887: if (_buffer == buffer) {
0888: if (bufferSwitcher != null) {
0889: if (buffer.isDirty())
0890: bufferSwitcher.repaint();
0891: else
0892: bufferSwitcher.updateBufferList();
0893: }
0894: }
0895: } else if (msg.getWhat() == BufferUpdate.MARKERS_CHANGED) {
0896: if (_buffer == buffer)
0897: textArea.getGutter().repaint();
0898: } else if (msg.getWhat() == BufferUpdate.PROPERTIES_CHANGED) {
0899: if (_buffer == buffer && buffer.isLoaded()) {
0900: textArea.propertiesChanged();
0901: if (view.getEditPane() == this )
0902: view.getStatus().updateBufferStatus();
0903: }
0904: } else if (msg.getWhat() == BufferUpdate.SAVED) {
0905: if (_buffer == buffer)
0906: textArea.propertiesChanged();
0907: }
0908: } //}}}
0909:
0910: //}}}
0911:
0912: //{{{ StatusHandler class
0913: class StatusHandler implements StatusListener {
0914: public void statusChanged(
0915: org.gjt.sp.jedit.textarea.TextArea textArea, int flag,
0916: boolean value) {
0917: StatusBar status = view.getStatus();
0918: if (status == null)
0919: return;
0920:
0921: switch (flag) {
0922: case OVERWRITE_CHANGED:
0923: status.setMessageAndClear(jEdit.getProperty(
0924: "view.status.overwrite-changed",
0925: new Integer[] { value ? 1 : 0 }));
0926: break;
0927: case MULTI_SELECT_CHANGED:
0928: status.setMessageAndClear(jEdit.getProperty(
0929: "view.status.multi-changed",
0930: new Integer[] { value ? 1 : 0 }));
0931: break;
0932: case RECT_SELECT_CHANGED:
0933: status.setMessageAndClear(jEdit.getProperty(
0934: "view.status.rect-select-changed",
0935: new Integer[] { value ? 1 : 0 }));
0936: break;
0937: }
0938:
0939: status.updateMiscStatus();
0940: }
0941:
0942: public void bracketSelected(
0943: org.gjt.sp.jedit.textarea.TextArea textArea, int line,
0944: String text) {
0945: StatusBar status = view.getStatus();
0946: if (status == null)
0947: return;
0948:
0949: status
0950: .setMessageAndClear(jEdit.getProperty(
0951: "view.status.bracket", new Object[] { line,
0952: text }));
0953: }
0954:
0955: public void narrowActive(
0956: org.gjt.sp.jedit.textarea.TextArea textArea) {
0957: StatusBar status = view.getStatus();
0958: if (status == null)
0959: return;
0960:
0961: status.setMessageAndClear(jEdit
0962: .getProperty("view.status.narrow"));
0963: }
0964: } //}}}
0965:
0966: //{{{ MarkerHighlight class
0967: class MarkerHighlight extends TextAreaExtension {
0968: private boolean markerHighlight;
0969: private Color markerHighlightColor;
0970:
0971: //{{{ getMarkerHighlightColor() method
0972: public Color getMarkerHighlightColor() {
0973: return markerHighlightColor;
0974: } //}}}
0975:
0976: //{{{ setMarkerHighlightColor() method
0977: public void setMarkerHighlightColor(Color markerHighlightColor) {
0978: this .markerHighlightColor = markerHighlightColor;
0979: } //}}}
0980:
0981: //{{{ isMarkerHighlightEnabled() method
0982: public boolean isMarkerHighlightEnabled() {
0983: return markerHighlight;
0984: } //}}}
0985:
0986: //{{{ isMarkerHighlightEnabled()
0987: public void setMarkerHighlightEnabled(boolean markerHighlight) {
0988: this .markerHighlight = markerHighlight;
0989: } //}}}
0990:
0991: //{{{ paintValidLine() method
0992: public void paintValidLine(Graphics2D gfx, int screenLine,
0993: int physicalLine, int start, int end, int y) {
0994: if (isMarkerHighlightEnabled()) {
0995: Buffer buffer = (Buffer) textArea.getBuffer();
0996: if (buffer.getMarkerInRange(start, end) != null) {
0997: gfx.setColor(getMarkerHighlightColor());
0998: FontMetrics fm = textArea.getPainter()
0999: .getFontMetrics();
1000: gfx.fillRect(0, y, textArea.getGutter().getWidth(),
1001: fm.getHeight());
1002: }
1003: }
1004: } //}}}
1005:
1006: //{{{ getToolTipText() method
1007: public String getToolTipText(int x, int y) {
1008: if (isMarkerHighlightEnabled()) {
1009: int lineHeight = textArea.getPainter().getFontMetrics()
1010: .getHeight();
1011: if (lineHeight == 0)
1012: return null;
1013:
1014: int line = y / lineHeight;
1015: int start = textArea.getScreenLineStartOffset(line);
1016: int end = textArea.getScreenLineEndOffset(line);
1017: if (start == -1 || end == -1)
1018: return null;
1019:
1020: Buffer buffer = (Buffer) textArea.getBuffer();
1021: Marker marker = buffer.getMarkerInRange(start, end);
1022: if (marker != null) {
1023: char shortcut = marker.getShortcut();
1024: if (shortcut == '\0')
1025: return jEdit
1026: .getProperty("view.gutter.marker.no-name");
1027: else {
1028: String[] args = { String.valueOf(shortcut) };
1029: return jEdit.getProperty("view.gutter.marker",
1030: args);
1031: }
1032: }
1033: }
1034:
1035: return null;
1036: } //}}}
1037: } //}}}
1038: }
|