# HG changeset patch
# User wenzelm
# Date 1421695913 -3600
# Node ID 63cb603b5114cd476e60d4b37b9716944ed60568
# Parent  d43434c60d3a2d2a41e3ff2a0cfe9622e32668f5
more symmetric layout of main panel;
misc tuning;

diff -r d43434c60d3a -r 63cb603b5114 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Mon Jan 19 16:38:01 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Jan 19 20:31:53 2015 +0100
@@ -10,42 +10,56 @@
 
 import isabelle._
 
-import java.awt.{Dimension, Graphics2D, Point, Rectangle}
+import java.io.{File => JFile}
+import java.awt.{Color, Dimension, Graphics2D, Point, Rectangle}
 import java.awt.geom.{AffineTransform, Point2D}
+import javax.imageio.ImageIO
 import javax.swing.{JScrollPane, JComponent, SwingUtilities}
+import javax.swing.border.EmptyBorder
 
-import scala.swing.{Panel, ScrollPane}
+import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser, Panel, ScrollPane}
 import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent}
 
 
-class Graph_Panel(val visualizer: Visualizer) extends ScrollPane
+class Graph_Panel(val visualizer: Visualizer) extends BorderPanel
 {
-  panel =>
+  graph_panel =>
+
 
 
-  /* tooltips */
+  /** graph **/
 
-  tooltip = ""
+  /* painter */
 
-  override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
-    override def getToolTipText(event: java.awt.event.MouseEvent): String =
-      visualizer.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
-        case Some(node) =>
-          visualizer.model.full_graph.get_node(node) match {
-            case Nil => null
-            case content => visualizer.make_tooltip(panel.peer, event.getX, event.getY, content)
-          }
-        case None => null
-      }
+  private val painter = new Panel
+  {
+    override def paint(gfx: Graphics2D)
+    {
+      super.paintComponent(gfx)
+
+      gfx.setColor(visualizer.background_color)
+      gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
+
+      gfx.transform(Transform())
+      visualizer.paint_all_visible(gfx)
+    }
   }
 
-
-  /* scrolling */
+  def set_preferred_size()
+  {
+    val box = visualizer.bounding_box()
+    val s = Transform.scale_discrete
+    painter.preferredSize = new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt)
+    painter.revalidate()
+  }
 
-  horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
-  verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
-
-  peer.getVerticalScrollBar.setUnitIncrement(10)
+  def refresh()
+  {
+    if (painter != null) {
+      set_preferred_size()
+      painter.repaint()
+    }
+  }
 
   def scroll_to_node(node: Graph_Display.Node)
   {
@@ -58,47 +72,54 @@
     val q =
       t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null)
 
-    paint_panel.peer.scrollRectToVisible(
+    painter.peer.scrollRectToVisible(
       new Rectangle(p.getX.toInt, p.getY.toInt,
         (q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt))
   }
 
 
-  /* painting */
+  /* scrollable graph pane */
+
+  private val graph_pane: ScrollPane = new ScrollPane(painter) {
+    tooltip = ""
 
-  private class Paint_Panel extends Panel
-  {
-    def set_preferred_size()
-    {
-      val box = visualizer.bounding_box()
-      val s = Transform.scale_discrete
-
-      preferredSize =
-        new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt)
-
-      revalidate()
+    override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
+      override def getToolTipText(event: java.awt.event.MouseEvent): String =
+        visualizer.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
+          case Some(node) =>
+            visualizer.model.full_graph.get_node(node) match {
+              case Nil => null
+              case content =>
+                visualizer.make_tooltip(graph_pane.peer, event.getX, event.getY, content)
+            }
+          case None => null
+        }
     }
 
-    override def paint(gfx: Graphics2D)
+    horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
+    verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
+
+    listenTo(mouse.moves)
+    listenTo(mouse.clicks)
+    reactions +=
     {
-      super.paintComponent(gfx)
-      gfx.setColor(visualizer.background_color)
-      gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
-      gfx.transform(Transform())
+      case MousePressed(_, p, _, _, _) =>
+        Mouse_Interaction.pressed(p)
+        painter.repaint()
+      case MouseDragged(_, to, _) =>
+        Mouse_Interaction.dragged(to)
+        painter.repaint()
+      case e @ MouseClicked(_, p, m, n, _) =>
+        Mouse_Interaction.clicked(p, m, n, SwingUtilities.isRightMouseButton(e.peer))
+        painter.repaint()
+    }
 
-      visualizer.paint_all_visible(gfx)
-    }
+    contents = painter
   }
-  private val paint_panel = new Paint_Panel
-  contents = paint_panel
+  graph_pane.peer.getVerticalScrollBar.setUnitIncrement(10)
 
-  def refresh()
-  {
-    if (paint_panel != null) {
-      paint_panel.set_preferred_size()
-      paint_panel.repaint()
-    }
-  }
+
+  /* transform */
 
   val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
 
@@ -109,11 +130,6 @@
     refresh()
   }
 
-  rescale(1.0)
-
-
-  /* transform */
-
   def fit_to_window()
   {
     Transform.fit_to_window()
@@ -156,7 +172,7 @@
     def pane_to_graph_coordinates(at: Point2D): Point2D =
     {
       val s = Transform.scale_discrete
-      val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null)
+      val p = Transform().inverseTransform(graph_pane.peer.getViewport.getViewPosition, null)
 
       p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s)
       p
@@ -166,23 +182,8 @@
 
   /* interaction */
 
-  visualizer.model.Colors.events += { case _ => repaint() }
-  visualizer.model.Mutators.events += { case _ => repaint() }
-
-  listenTo(mouse.moves)
-  listenTo(mouse.clicks)
-  reactions +=
-  {
-    case MousePressed(_, p, _, _, _) =>
-      Mouse_Interaction.pressed(p)
-      repaint()
-    case MouseDragged(_, to, _) =>
-      Mouse_Interaction.dragged(to)
-      repaint()
-    case e @ MouseClicked(_, p, m, n, _) =>
-      Mouse_Interaction.clicked(p, m, n, SwingUtilities.isRightMouseButton(e.peer))
-      repaint()
-  }
+  visualizer.model.Colors.events += { case _ => painter.repaint() }
+  visualizer.model.Mutators.events += { case _ => painter.repaint() }
 
   private object Mouse_Interaction
   {
@@ -217,9 +218,9 @@
 
       (p, d) match {
         case (Nil, Nil) =>
-          val r = panel.peer.getViewport.getViewRect
+          val r = graph_pane.peer.getViewport.getViewRect
           r.translate(- dx, - dy)
-          paint_panel.peer.scrollRectToVisible(r)
+          painter.peer.scrollRectToVisible(r)
 
         case (Nil, ds) =>
           ds.foreach(d => visualizer.translate_vertex(d, dx / s, dy / s))
@@ -239,8 +240,8 @@
         if (right_click) {
           // FIXME
           if (false) {
-            val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get())
-            menu.show(panel.peer, at.x, at.y)
+            val menu = Popups(graph_panel, visualizer.find_node(c), visualizer.Selection.get())
+            menu.show(graph_pane.peer, at.x, at.y)
           }
         }
         else {
@@ -261,4 +262,108 @@
       }
     }
   }
+
+
+
+  /** controls **/
+
+  private val mutator_dialog =
+    new Mutator_Dialog(visualizer, visualizer.model.Mutators, "Filters", "Hide", false)
+  private val color_dialog =
+    new Mutator_Dialog(visualizer, visualizer.model.Colors, "Colorations")
+
+  private val chooser = new FileChooser {
+    fileSelectionMode = FileChooser.SelectionMode.FilesOnly
+    title = "Save image (.png or .pdf)"
+  }
+
+  private val controls =
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+      new CheckBox() {
+        selected = visualizer.show_content
+        action = Action("Show content") {
+          visualizer.show_content = selected
+          visualizer.update_layout()
+          refresh()
+        }
+        tooltip = "Show full node content within graph layout"
+      },
+      new CheckBox() {
+        selected = visualizer.show_arrow_heads
+        action = Action("Show arrow heads") {
+          visualizer.show_arrow_heads = selected
+          painter.repaint()
+        }
+        tooltip = "Draw edges with explicit arrow heads"
+      },
+      new CheckBox() {
+        selected = visualizer.show_dummies
+        action = Action("Show dummies") {
+          visualizer.show_dummies = selected
+          painter.repaint()
+        }
+        tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging"
+      },
+      new Button {
+        action = Action("Save image") {
+          chooser.showSaveDialog(this) match {
+            case FileChooser.Result.Approve => save_file(chooser.selectedFile)
+            case _ =>
+          }
+        }
+        tooltip = "Save current graph layout as PNG or PDF"
+      },
+      zoom,
+      new Button {
+        action = Action("Fit to window") { fit_to_window() }
+        tooltip = "Zoom to fit window width and height"
+      },
+      new Button {
+        action = Action("Update layout") {
+          visualizer.update_layout()
+          refresh()
+        }
+        tooltip = "Regenerate graph layout according to built-in algorithm"
+      })
+    /* FIXME
+      new Button { action = Action("Colorations") { color_dialog.open } },
+      new Button { action = Action("Filters") { mutator_dialog.open } }
+    */
+
+
+  /* save file */
+
+  private def save_file(file: JFile)
+  {
+    val box = visualizer.bounding_box()
+    val w = box.width.ceil.toInt
+    val h = box.height.ceil.toInt
+
+    def paint(gfx: Graphics2D)
+    {
+      gfx.setColor(Color.WHITE)
+      gfx.fillRect(0, 0, w, h)
+      gfx.translate(- box.x, - box.y)
+      visualizer.paint_all_visible(gfx)
+    }
+
+    try {
+      val name = file.getName
+      if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h)
+      else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h)
+      else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
+    }
+    catch {
+      case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
+    }
+  }
+
+
+
+  /** main layout **/
+
+  layout(graph_pane) = BorderPanel.Position.Center
+  layout(controls) = BorderPanel.Position.North
+
+  rescale(1.0)
 }
diff -r d43434c60d3a -r 63cb603b5114 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Mon Jan 19 16:38:01 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Mon Jan 19 20:31:53 2015 +0100
@@ -10,117 +10,30 @@
 
 import isabelle._
 
-import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser, SplitPane, Orientation}
-
-import java.io.{File => JFile}
-import java.awt.{Color, Graphics2D}
-import javax.imageio.ImageIO
-import javax.swing.border.EmptyBorder
-import javax.swing.JComponent
+import scala.swing.{SplitPane, Orientation}
 
 
-class Main_Panel(model: Model, visualizer: Visualizer) extends BorderPanel
+class Main_Panel(visualizer: Visualizer) extends SplitPane(Orientation.Vertical)
 {
+  oneTouchExpandable = true
+
   val graph_panel = new Graph_Panel(visualizer)
   val tree_panel = new Tree_Panel(visualizer, graph_panel)
 
+  if (visualizer.options.bool("graphview_swap_panels")) {
+    leftComponent = tree_panel
+    rightComponent = graph_panel
+  }
+  else {
+    leftComponent = graph_panel
+    rightComponent = tree_panel
+  }
+
   def update_layout()
   {
     visualizer.update_layout()
     tree_panel.refresh()
     graph_panel.refresh()
   }
-
-  val split_pane =
-    if (visualizer.options.bool("graphview_swap_panels"))
-      new SplitPane(Orientation.Vertical, tree_panel, graph_panel)
-    else
-      new SplitPane(Orientation.Vertical, graph_panel, tree_panel)
-  split_pane.oneTouchExpandable = true
-
-  val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false)
-
-  val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations")
-
-  private val chooser = new FileChooser()
-  chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
-  chooser.title = "Save image (.png or .pdf)"
-
-  val controls =
-    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-      new CheckBox() {
-        selected = visualizer.show_content
-        action = Action("Show content") {
-          visualizer.show_content = selected
-          update_layout()
-        }
-        tooltip = "Show full node content within graph layout"
-      },
-      new CheckBox() {
-        selected = visualizer.show_arrow_heads
-        action = Action("Show arrow heads") {
-          visualizer.show_arrow_heads = selected
-          graph_panel.repaint()
-        }
-        tooltip = "Draw edges with explicit arrow heads"
-      },
-      new CheckBox() {
-        selected = visualizer.show_dummies
-        action = Action("Show dummies") {
-          visualizer.show_dummies = selected
-          graph_panel.repaint()
-        }
-        tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging"
-      },
-      new Button {
-        action = Action("Save image") {
-          chooser.showSaveDialog(this) match {
-            case FileChooser.Result.Approve => export(chooser.selectedFile)
-            case _ =>
-          }
-        }
-        tooltip = "Save current graph layout as PNG or PDF"
-      },
-      graph_panel.zoom,
-      new Button {
-        action = Action("Fit to window") { graph_panel.fit_to_window() }
-        tooltip = "Zoom to fit window width and height"
-      },
-      new Button {
-        action = Action("Update layout") { update_layout() }
-        tooltip = "Regenerate graph layout according to built-in algorithm"
-      })
-    /* FIXME
-      new Button { action = Action("Colorations") { color_dialog.open } },
-      new Button { action = Action("Filters") { mutator_dialog.open } }
-    */
-
-  layout(split_pane) = BorderPanel.Position.Center
-  layout(controls) = BorderPanel.Position.North
   update_layout()
-
-  private def export(file: JFile)
-  {
-    val box = visualizer.bounding_box()
-    val w = box.width.ceil.toInt
-    val h = box.height.ceil.toInt
-
-    def paint(gfx: Graphics2D)
-    {
-      gfx.setColor(Color.WHITE)
-      gfx.fillRect(0, 0, w, h)
-      gfx.translate(- box.x, - box.y)
-      visualizer.paint_all_visible(gfx)
-    }
-
-    try {
-      val name = file.getName
-      if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h)
-      else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h)
-      else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
-    }
-    catch {
-      case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
-    }
-  }
 }
diff -r d43434c60d3a -r 63cb603b5114 src/Tools/Graphview/popups.scala
--- a/src/Tools/Graphview/popups.scala	Mon Jan 19 16:38:01 2015 +0100
+++ b/src/Tools/Graphview/popups.scala	Mon Jan 19 20:31:53 2015 +0100
@@ -17,11 +17,11 @@
 object Popups
 {
   def apply(
-    panel: Graph_Panel,
+    graph_panel: Graph_Panel,
     mouse_node: Option[Graph_Display.Node],
     selected_nodes: List[Graph_Display.Node]): JPopupMenu =
   {
-    val visualizer = panel.visualizer
+    val visualizer = graph_panel.visualizer
 
     val add_mutator = visualizer.model.Mutators.add _
     val visible_graph = visualizer.visible_graph
@@ -138,7 +138,9 @@
       popup.add(new JPopupMenu.Separator)
     }
 
-    popup.add(new MenuItem(new Action("Fit to window") { def apply = panel.fit_to_window() }).peer)
+    popup.add(new MenuItem(new Action("Fit to window") {
+      def apply = graph_panel.fit_to_window() }).peer
+    )
 
     popup
   }
diff -r d43434c60d3a -r 63cb603b5114 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 19 16:38:01 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 19 20:31:53 2015 +0100
@@ -86,7 +86,7 @@
           override def current_color = view.getTextArea.getPainter.getLineHighlightColor
           override def error_color = PIDE.options.color_value("error_color")
         }
-        new isabelle.graphview.Main_Panel(model, visualizer)
+        new isabelle.graphview.Main_Panel(visualizer)
       case Exn.Exn(exn) => new TextArea(Exn.message(exn))
     }
   set_content(graphview)