isabelle: src/Tools/Graphview/main_panel.scala@18d383f41477 (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
59459 985fc55e9f27 clarified module name; wenzelm parents: 59412 diff changeset	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 63cb603b5114 more symmetric layout of main panel; wenzelm parents: 59406 diff changeset	18	oneTouchExpandable = true
63cb603b5114 more symmetric layout of main panel; wenzelm parents: 59406 diff changeset	19
59459 985fc55e9f27 clarified module name; wenzelm parents: 59412 diff changeset	20	val graph_panel = new Graph_Panel(graphview)
985fc55e9f27 clarified module name; wenzelm parents: 59412 diff changeset	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: 50471 diff changeset	22
59412 0426b53a5d54 always swap panels, which leads to slightly better GUI layout; wenzelm parents: 59408 diff changeset	23	leftComponent = tree_panel
0426b53a5d54 always swap panels, which leads to slightly better GUI layout; wenzelm parents: 59408 diff changeset	24	rightComponent = graph_panel
59408 63cb603b5114 more symmetric layout of main panel; wenzelm parents: 59406 diff changeset	25
59392 02bacfc31446 support for tree view on graph nodes; wenzelm parents: 59384 diff changeset	26	def update_layout()
02bacfc31446 support for tree view on graph nodes; wenzelm parents: 59384 diff changeset	27	{
59459 985fc55e9f27 clarified module name; wenzelm parents: 59412 diff changeset	28	graphview.update_layout()
59392 02bacfc31446 support for tree view on graph nodes; wenzelm parents: 59384 diff changeset	29	tree_panel.refresh()
02bacfc31446 support for tree view on graph nodes; wenzelm parents: 59384 diff changeset	30	graph_panel.refresh()
02bacfc31446 support for tree view on graph nodes; wenzelm parents: 59384 diff changeset	31	}
02bacfc31446 support for tree view on graph nodes; wenzelm parents: 59384 diff changeset	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	}

author	wenzelm
	Fri, 25 Jan 2019 15:57:24 +0100
changeset 69740	18d383f41477
parent 59459	985fc55e9f27
child 73340	0ffcad1f6130
permissions	-rw-r--r--