equal
deleted
inserted
replaced
11 import isabelle._ |
11 import isabelle._ |
12 |
12 |
13 import scala.swing.{SplitPane, Orientation} |
13 import scala.swing.{SplitPane, Orientation} |
14 |
14 |
15 |
15 |
16 class Main_Panel(graphview: Graphview) extends SplitPane(Orientation.Vertical) |
16 class Main_Panel(graphview: Graphview) extends SplitPane(Orientation.Vertical) { |
17 { |
|
18 oneTouchExpandable = true |
17 oneTouchExpandable = true |
19 |
18 |
20 val graph_panel = new Graph_Panel(graphview) |
19 val graph_panel = new Graph_Panel(graphview) |
21 val tree_panel = new Tree_Panel(graphview, graph_panel) |
20 val tree_panel = new Tree_Panel(graphview, graph_panel) |
22 |
21 |
23 leftComponent = tree_panel |
22 leftComponent = tree_panel |
24 rightComponent = graph_panel |
23 rightComponent = graph_panel |
25 |
24 |
26 def update_layout(): Unit = |
25 def update_layout(): Unit = { |
27 { |
|
28 graphview.update_layout() |
26 graphview.update_layout() |
29 tree_panel.refresh() |
27 tree_panel.refresh() |
30 graph_panel.refresh() |
28 graph_panel.refresh() |
31 } |
29 } |
32 update_layout() |
30 update_layout() |