equal
deleted
inserted
replaced
12 import scala.swing.{TextArea, ScrollPane} |
12 import scala.swing.{TextArea, ScrollPane} |
13 |
13 |
14 import org.gjt.sp.jedit.View |
14 import org.gjt.sp.jedit.View |
15 |
15 |
16 |
16 |
17 class Raw_Output_Dockable(view: View, position: String) extends Dockable(view, position) |
17 class Raw_Output_Dockable(view: View, position: String) extends Dockable(view, position) { |
18 { |
|
19 private val text_area = new TextArea |
18 private val text_area = new TextArea |
20 set_content(new ScrollPane(text_area)) |
19 set_content(new ScrollPane(text_area)) |
21 |
20 |
22 |
21 |
23 /* main */ |
22 /* main */ |