| author | blanchet | 
| Thu, 25 Jun 2015 12:41:43 +0200 | |
| changeset 60568 | a9b71c82647b | 
| parent 59459 | 985fc55e9f27 | 
| child 73340 | 0ffcad1f6130 | 
| permissions | -rw-r--r-- | 
| 59202 | 1 | /* Title: Tools/Graphview/main_panel.scala | 
| 49557 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 2 | Author: Markus Kaiser, TU Muenchen | 
| 59240 | 3 | Author: Makarius | 
| 49557 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 4 | |
| 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 5 | Graph Panel wrapper. | 
| 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 6 | */ | 
| 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 7 | |
| 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 8 | package isabelle.graphview | 
| 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 9 | |
| 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 10 | |
| 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 11 | import isabelle._ | 
| 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 12 | |
| 59408 | 13 | import scala.swing.{SplitPane, Orientation}
 | 
| 49557 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 14 | |
| 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 15 | |
| 59459 | 16 | class Main_Panel(graphview: Graphview) extends SplitPane(Orientation.Vertical) | 
| 49557 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 17 | {
 | 
| 59408 | 18 | oneTouchExpandable = true | 
| 19 | ||
| 59459 | 20 | val graph_panel = new Graph_Panel(graphview) | 
| 21 | val tree_panel = new Tree_Panel(graphview, graph_panel) | |
| 50472 
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
 wenzelm parents: 
50471diff
changeset | 22 | |
| 59412 
0426b53a5d54
always swap panels, which leads to slightly better GUI layout;
 wenzelm parents: 
59408diff
changeset | 23 | leftComponent = tree_panel | 
| 
0426b53a5d54
always swap panels, which leads to slightly better GUI layout;
 wenzelm parents: 
59408diff
changeset | 24 | rightComponent = graph_panel | 
| 59408 | 25 | |
| 59392 | 26 | def update_layout() | 
| 27 |   {
 | |
| 59459 | 28 | graphview.update_layout() | 
| 59392 | 29 | tree_panel.refresh() | 
| 30 | graph_panel.refresh() | |
| 31 | } | |
| 32 | update_layout() | |
| 49557 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
 Markus Kaiser <markus.kaiser@in.tum.de> parents: diff
changeset | 33 | } |