src/Tools/Graphview/main_panel.scala
author wenzelm
Wed, 22 Jan 2025 22:22:19 +0100
changeset 81954 6f2bcdfa9a19
parent 75393 87ebf5a50283
permissions -rw-r--r--
misc tuning: more concise operations on prems (without change of exceptions); discontinue odd clone Drule.cprems_of (see also 991a3feaf270);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59202
711c2446dc9d clarified source location;
wenzelm
parents: 58452
diff changeset
     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
e411afcfaa29 tuned headers;
wenzelm
parents: 59233
diff changeset
     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
63cb603b5114 more symmetric layout of main panel;
wenzelm
parents: 59406
diff changeset
    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
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    16
class Main_Panel(graphview: Graphview) extends SplitPane(Orientation.Vertical) {
59408
63cb603b5114 more symmetric layout of main panel;
wenzelm
parents: 59406
diff changeset
    17
  oneTouchExpandable = true
63cb603b5114 more symmetric layout of main panel;
wenzelm
parents: 59406
diff changeset
    18
59459
985fc55e9f27 clarified module name;
wenzelm
parents: 59412
diff changeset
    19
  val graph_panel = new Graph_Panel(graphview)
985fc55e9f27 clarified module name;
wenzelm
parents: 59412
diff changeset
    20
  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: 50471
diff changeset
    21
59412
0426b53a5d54 always swap panels, which leads to slightly better GUI layout;
wenzelm
parents: 59408
diff changeset
    22
  leftComponent = tree_panel
0426b53a5d54 always swap panels, which leads to slightly better GUI layout;
wenzelm
parents: 59408
diff changeset
    23
  rightComponent = graph_panel
59408
63cb603b5114 more symmetric layout of main panel;
wenzelm
parents: 59406
diff changeset
    24
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    25
  def update_layout(): Unit = {
59459
985fc55e9f27 clarified module name;
wenzelm
parents: 59412
diff changeset
    26
    graphview.update_layout()
59392
02bacfc31446 support for tree view on graph nodes;
wenzelm
parents: 59384
diff changeset
    27
    tree_panel.refresh()
02bacfc31446 support for tree view on graph nodes;
wenzelm
parents: 59384
diff changeset
    28
    graph_panel.refresh()
02bacfc31446 support for tree view on graph nodes;
wenzelm
parents: 59384
diff changeset
    29
  }
02bacfc31446 support for tree view on graph nodes;
wenzelm
parents: 59384
diff changeset
    30
  update_layout()
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    31
}