File: Reset_TextArea.bsh

package info (click to toggle)
jedit 5.3.0%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 14,252 kB
  • ctags: 11,190
  • sloc: java: 98,480; xml: 94,070; makefile: 52; sh: 42; cpp: 6; python: 6
file content (16 lines) | stat: -rw-r--r-- 504 bytes parent folder | download | duplicates (6) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
 
/** Reset_TextArea.bsh
    A macro that performs a split and an unsplit of the current TextArea.
	Useful for those occasions when your textarea is corrupt (painting the
	incorrect characters on the screen).
*/
import javax.swing.Timer;
view.splitVertically();
int delay = 100; //milliseconds
ActionListener taskPerformer = new ActionListener() {
  public void actionPerformed(ActionEvent evt) {
          view.unsplitCurrent();
  }
};
t = new Timer(delay, taskPerformer);
t.setRepeats(false);
t.start();