equal
deleted
inserted
replaced
16 |
16 |
17 |
17 |
18 class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String) |
18 class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String) |
19 { |
19 { |
20 private val text_area = new TextArea("Isabelle session") |
20 private val text_area = new TextArea("Isabelle session") |
|
21 text_area.editable = false |
21 set_content(new ScrollPane(text_area)) |
22 set_content(new ScrollPane(text_area)) |
22 |
23 |
23 |
24 |
24 /* main actor */ |
25 /* main actor */ |
25 |
26 |