isabelle: src/Tools/Graphview/main_panel.scala@ca56952b7322 (annotated)

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	}

author	wenzelm
	Sun, 03 Sep 2023 16:44:07 +0200
changeset 78639	ca56952b7322
parent 75393	87ebf5a50283
permissions	-rw-r--r--