equal
deleted
inserted
replaced
12 import scala.actors.Actor._ |
12 import scala.actors.Actor._ |
13 |
13 |
14 import scala.swing.Button |
14 import scala.swing.Button |
15 import scala.swing.event.ButtonClicked |
15 import scala.swing.event.ButtonClicked |
16 |
16 |
17 import java.lang.System |
|
18 import java.awt.BorderLayout |
17 import java.awt.BorderLayout |
19 import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent} |
18 import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent} |
20 |
19 |
21 import org.gjt.sp.jedit.View |
20 import org.gjt.sp.jedit.View |
22 |
21 |