src/Tools/Graphview/main_panel.scala
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (19 months ago)
changeset 67835 c8e4ee2b5482
parent 59459 985fc55e9f27
permissions -rw-r--r--
tuned imports;
wenzelm@59202
     1
/*  Title:      Tools/Graphview/main_panel.scala
markus@49557
     2
    Author:     Markus Kaiser, TU Muenchen
wenzelm@59240
     3
    Author:     Makarius
markus@49557
     4
markus@49557
     5
Graph Panel wrapper.
markus@49557
     6
*/
markus@49557
     7
markus@49557
     8
package isabelle.graphview
markus@49557
     9
markus@49557
    10
markus@49557
    11
import isabelle._
markus@49557
    12
wenzelm@59408
    13
import scala.swing.{SplitPane, Orientation}
markus@49557
    14
markus@49557
    15
wenzelm@59459
    16
class Main_Panel(graphview: Graphview) extends SplitPane(Orientation.Vertical)
markus@49557
    17
{
wenzelm@59408
    18
  oneTouchExpandable = true
wenzelm@59408
    19
wenzelm@59459
    20
  val graph_panel = new Graph_Panel(graphview)
wenzelm@59459
    21
  val tree_panel = new Tree_Panel(graphview, graph_panel)
wenzelm@50472
    22
wenzelm@59412
    23
  leftComponent = tree_panel
wenzelm@59412
    24
  rightComponent = graph_panel
wenzelm@59408
    25
wenzelm@59392
    26
  def update_layout()
wenzelm@59392
    27
  {
wenzelm@59459
    28
    graphview.update_layout()
wenzelm@59392
    29
    tree_panel.refresh()
wenzelm@59392
    30
    graph_panel.refresh()
wenzelm@59392
    31
  }
wenzelm@59392
    32
  update_layout()
markus@49557
    33
}