more explicit Layout.Info: size and content;
allow multi-line vertex label, based on content;
misc tuning;

--- a/src/Tools/Graphview/etc/options	Sat Jan 17 16:40:10 2015 +0100
+++ b/src/Tools/Graphview/etc/options	Sat Jan 17 22:20:57 2015 +0100
@@ -20,3 +20,6 @@
 public option graphview_iterations_rubberband : int = 10
   -- "number of iterations for rubberband method"
 
+public option graphview_content_margin : int = 60
+  -- "margin for node content pretty-printing"
+

--- a/src/Tools/Graphview/layout.scala	Sat Jan 17 16:40:10 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Sat Jan 17 22:20:57 2015 +0100
@@ -55,12 +55,18 @@
   case class Node(node: Graph_Display.Node) extends Vertex
   case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex
 
-  object Point { val zero: Point = Point(0.0, 0.0) }
-  case class Point(x: Double, y: Double)
+  sealed case class Info(
+    x: Double, y: Double, width2: Double, height2: Double, lines: List[String])
+  {
+    def left: Double = x - width2
+    def right: Double = x + width2
+    def width: Double = 2 * width2
+    def height: Double = 2 * height2
+  }
 
-  type Graph = isabelle.Graph[Vertex, Point]
+  type Graph = isabelle.Graph[Vertex, Info]
 
-  def make_graph(entries: List[((Vertex, Point), List[Vertex])]): Graph =
+  def make_graph(entries: List[((Vertex, Info), List[Vertex])]): Graph =
     isabelle.Graph.make(entries)(Vertex.Ordering)
 
   val empty_graph: Graph = make_graph(Nil)
@@ -68,14 +74,11 @@
 
   /* vertex x coordinate */
 
-  private def vertex_left(metrics: Metrics, graph: Graph, v: Vertex): Double =
-    graph.get_node(v).x - metrics.box_width2(v)
-
-  private def vertex_right(metrics: Metrics, graph: Graph, v: Vertex): Double =
-    graph.get_node(v).x + metrics.box_width2(v)
+  private def vertex_left(graph: Graph, v: Vertex) = graph.get_node(v).left
+  private def vertex_right(graph: Graph, v: Vertex) = graph.get_node(v).right
 
   private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph =
-    if (dx == 0.0) graph else graph.map_node(v, p => Point(p.x + dx, p.y))
+    if (dx == 0.0) graph else graph.map_node(v, info => info.copy(x = info.x + dx))
 
 
   /* layout */
@@ -86,7 +89,9 @@
   private type Levels = Map[Vertex, Int]
   private val empty_levels: Levels = Map.empty
 
-  def make(options: Options, metrics: Metrics, input_graph: Graph_Display.Graph): Layout =
+  def make(options: Options, metrics: Metrics,
+    node_text: (Graph_Display.Node, XML.Body) => String,
+    input_graph: Graph_Display.Graph): Layout =
   {
     if (input_graph.is_empty) empty
     else {
@@ -95,7 +100,12 @@
       val initial_graph =
         make_graph(
           input_graph.iterator.map(
-            { case (a, (_, (_, bs))) => ((Node(a), Point.zero), bs.toList.map(Node(_))) }).toList)
+            { case (a, (content, (_, bs))) =>
+                val lines = split_lines(node_text(a, content))
+                val w2 = metrics.node_width2(lines)
+                val h2 = metrics.node_height2(lines.length)
+                ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node(_)))
+            }).toList)
 
       val initial_levels: Levels =
         (empty_levels /: initial_graph.topological_order) {
@@ -108,6 +118,8 @@
 
       /* graph with dummies */
 
+      val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil)
+
       val (dummy_graph, dummy_levels) =
         ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
             case ((graph, levels), (node1, node2)) =>
@@ -122,7 +134,7 @@
 
                 val levels1 = (levels /: dummies_levels)(_ + _)
                 val graph1 =
-                  ((graph /: dummies)(_.new_node(_, Point.zero)).del_edge(v1, v2) /:
+                  ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /:
                     (v1 :: dummies ::: List(v2)).sliding(2)) {
                       case (g, List(a, b)) => g.add_edge(a, b) }
                 (graph1, levels1)
@@ -137,12 +149,22 @@
       val levels_graph: Graph =
         (((dummy_graph, 0.0) /: levels) {
           case ((graph, y), level) =>
+            val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length }
             val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size }
-            ((((graph, 0.0) /: level) {
-              case ((g, x), v) =>
-                val w2 = metrics.box_width2(v)
-                (g.map_node(v, _ => Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
-            })._1, y + metrics.box_height(num_edges))
+
+            val y1 = y + metrics.node_height2(num_lines)
+
+            val graph1 =
+              (((graph, 0.0) /: level) { case ((g, x), v) =>
+                val info = g.get_node(v)
+                val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
+                val x1 = x + info.width + metrics.gap
+                (g1, x1)
+              })._1
+
+            val y2 = y1 + metrics.level_height2(num_lines, num_edges)
+
+            (graph1, y2)
         })._1
 
 
@@ -224,9 +246,9 @@
   private class Region(val content: List[Vertex])
   {
     def distance(metrics: Metrics, graph: Graph, that: Region): Double =
-      vertex_left(metrics, graph, that.content.head) -
-      vertex_right(metrics, graph, this.content.last) -
-      metrics.box_gap
+      vertex_left(graph, that.content.head) -
+      vertex_right(graph, this.content.last) -
+      metrics.gap
 
     def deflection(graph: Graph, top_down: Boolean): Double =
       ((for (a <- content.iterator) yield {
@@ -317,9 +339,7 @@
   private def rubberband(
     options: Options, metrics: Metrics, levels: List[Level], graph: Graph): Graph =
   {
-    val gap = metrics.box_gap
-    def left(g: Graph, v: Vertex) = vertex_left(metrics, g, v)
-    def right(g: Graph, v: Vertex) = vertex_right(metrics, g, v)
+    val gap = metrics.gap
 
     (graph /: (1 to options.int("graphview_iterations_rubberband"))) { case (graph, _) =>
       (graph /: levels) { case (graph, level) =>
@@ -327,8 +347,8 @@
         (graph /: level.iterator.zipWithIndex) {
           case (g, (v, i)) =>
             val d = force_weight(g, v)
-            if (d < 0.0 && (i == 0 || right(g, level(i - 1)) + gap < left(g, v) + d) ||
-                d > 0.0 && (i == m || left(g, level(i + 1)) - gap > right(g, v) + d))
+            if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
+                d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
               move_vertex(g, v, d.round.toDouble)
             else g
         }
@@ -344,34 +364,40 @@
 {
   /* vertex coordinates */
 
-  def get_vertex(v: Layout.Vertex): Layout.Point =
-    if (output_graph.defined(v)) output_graph.get_node(v)
-    else Layout.Point.zero
-
   def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout =
   {
     if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this
     else {
-      val output_graph1 = output_graph.map_node(v, p => Layout.Point(p.x + dx, p.y + dy))
+      val output_graph1 =
+        output_graph.map_node(v, info => info.copy(x = info.x + dx, y = info.y + dy))
       new Layout(metrics, input_graph, output_graph1)
     }
   }
 
 
+  /* regular nodes */
+
+  def get_node(node: Graph_Display.Node): Layout.Info =
+    output_graph.get_node(Layout.Node(node))
+
+  def nodes_iterator: Iterator[Layout.Info] =
+    for ((_: Layout.Node, (info, _)) <- output_graph.iterator) yield info
+
+
   /* dummies */
 
-  def dummies_iterator: Iterator[Layout.Point] =
-    for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p
+  def dummies_iterator: Iterator[Layout.Info] =
+    for ((_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info
 
-  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] =
-    new Iterator[Layout.Point] {
+  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Info] =
+    new Iterator[Layout.Info] {
       private var index = 0
       def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
-      def next: Layout.Point =
+      def next: Layout.Info =
       {
-        val p = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
+        val info = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
         index += 1
-        p
+        info
       }
     }
 }

--- a/src/Tools/Graphview/main_panel.scala	Sat Jan 17 16:40:10 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Sat Jan 17 22:20:57 2015 +0100
@@ -40,12 +40,25 @@
   val options_panel =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
       new CheckBox() {
-        selected = visualizer.arrow_heads
-        action = Action("Arrow heads") { visualizer.arrow_heads = selected; graph_panel.repaint() }
+        selected = visualizer.show_content
+        action = Action("Show content") {
+          visualizer.show_content = selected
+          graph_panel.apply_layout()
+        }
+      },
+      new CheckBox() {
+        selected = visualizer.show_arrow_heads
+        action = Action("Show arrow heads") {
+          visualizer.show_arrow_heads = selected
+          graph_panel.repaint()
+        }
       },
       new CheckBox() {
         selected = visualizer.show_dummies
-        action = Action("Show dummies") { visualizer.show_dummies = selected; graph_panel.repaint() }
+        action = Action("Show dummies") {
+          visualizer.show_dummies = selected
+          graph_panel.repaint()
+        }
       },
       new Button {
         action = Action("Save image") {

--- a/src/Tools/Graphview/metrics.scala	Sat Jan 17 16:40:10 2015 +0100
+++ b/src/Tools/Graphview/metrics.scala	Sat Jan 17 22:20:57 2015 +0100
@@ -11,6 +11,7 @@
 
 import java.awt.{Font, RenderingHints}
 import java.awt.font.FontRenderContext
+import java.awt.geom.Rectangle2D
 
 
 object Metrics
@@ -28,27 +29,32 @@
 
 class Metrics private(val font: Font)
 {
-  def string_bounds(s: String) = font.getStringBounds(s, Metrics.font_render_context)
+  def string_bounds(s: String): Rectangle2D = font.getStringBounds(s, Metrics.font_render_context)
   private val mix = string_bounds("mix")
   val space_width = string_bounds(" ").getWidth
   def char_width: Double = mix.getWidth / 3
   def height: Double = mix.getHeight
   def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
-  def gap: Double = mix.getWidth
   def pad_x: Double = char_width * 1.5
   def pad_y: Double = char_width
 
-  def dummy_width2: Double = (pad_x / 2).ceil
+  def gap: Double = mix.getWidth.ceil
 
-  def box_width2(node: Graph_Display.Node): Double =
-    ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil
+  def dummy_size2: Double = (pad_x / 2).ceil
+
+  def node_width2(lines: List[String]): Double =
+    (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + pad_x) / 2).ceil
 
-  def box_width2(vertex: Layout.Vertex): Double =
-    vertex match {
-      case Layout.Node(node) => box_width2(node)
-      case _: Layout.Dummy => dummy_width2
-    }
-  def box_gap: Double = gap.ceil
-  def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
+  def node_height2(num_lines: Int): Double =
+    ((height.ceil * (num_lines max 1) + pad_y) / 2).ceil
+
+  def level_height2(num_lines: Int, num_edges: Int): Double =
+    (node_height2(num_lines) + gap) max (node_height2(1) * (num_edges max 5))
+
+  object Pretty_Metric extends Pretty.Metric
+  {
+    val unit = space_width max 1.0
+    def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit
+  }
 }
 

--- a/src/Tools/Graphview/shapes.scala	Sat Jan 17 16:40:10 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Sat Jan 17 22:20:57 2015 +0100
@@ -19,63 +19,48 @@
   private val default_stroke =
     new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
-  object Node
+  def shape(info: Layout.Info): Rectangle2D.Double =
+    new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height)
+
+  def paint_node(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
   {
-    def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double =
-    {
-      val metrics = visualizer.metrics
-      val p = visualizer.layout.get_vertex(Layout.Node(node))
-      val bounds = metrics.string_bounds(node.toString)
-      val w2 = ((bounds.getWidth + metrics.pad_x) / 2).ceil
-      val h2 = ((bounds.getHeight + metrics.pad_y) / 2).ceil
-      new Rectangle2D.Double(p.x - w2, p.y - h2, 2 * w2, 2 * h2)
-    }
+    val metrics = visualizer.metrics
+    val info = visualizer.layout.get_node(node)
+    val c = visualizer.node_color(node)
+    val s = shape(info)
+
+    gfx.setColor(c.background)
+    gfx.fill(s)
 
-    def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
-    {
-      val metrics = visualizer.metrics
-      val s = shape(visualizer, node)
-      val c = visualizer.node_color(node)
-      val bounds = metrics.string_bounds(node.toString)
+    gfx.setColor(c.border)
+    gfx.setStroke(default_stroke)
+    gfx.draw(s)
 
-      gfx.setColor(c.background)
-      gfx.fill(s)
+    gfx.setColor(c.foreground)
+    gfx.setFont(metrics.font)
 
-      gfx.setColor(c.border)
-      gfx.setStroke(default_stroke)
-      gfx.draw(s)
-
-      gfx.setColor(c.foreground)
-      gfx.setFont(metrics.font)
-      gfx.drawString(node.toString,
-        (s.getCenterX - bounds.getWidth / 2).round.toInt,
-        (s.getCenterY - bounds.getHeight / 2 + metrics.ascent).round.toInt)
-    }
+    val text_width =
+      (0.0 /: info.lines) { case (w, line) => w max metrics.string_bounds(line).getWidth }
+    val text_height =
+      (info.lines.length max 1) * metrics.height.ceil
+    val x = (s.getCenterX - text_width / 2).round.toInt
+    var y = (s.getCenterY - text_height / 2 + metrics.ascent).round.toInt
+    for (line <- info.lines) { gfx.drawString(line, x, y); y += metrics.height.ceil.toInt }
   }
 
-  object Dummy
+  def paint_dummy(gfx: Graphics2D, visualizer: Visualizer, info: Layout.Info)
   {
-    def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double =
-    {
-      val metrics = visualizer.metrics
-      val w = metrics.dummy_width2
-      new Rectangle2D.Double(d.x - w / 2, d.y - w / 2, w, w)
-    }
-
-    def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point)
-    {
-      gfx.setStroke(default_stroke)
-      gfx.setColor(visualizer.dummy_color)
-      gfx.draw(shape(visualizer, d))
-    }
+    gfx.setStroke(default_stroke)
+    gfx.setColor(visualizer.dummy_color)
+    gfx.draw(shape(info))
   }
 
   object Straight_Edge
   {
     def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
     {
-      val p = visualizer.layout.get_vertex(Layout.Node(edge._1))
-      val q = visualizer.layout.get_vertex(Layout.Node(edge._2))
+      val p = visualizer.layout.get_node(edge._1)
+      val q = visualizer.layout.get_node(edge._2)
       val ds =
       {
         val a = p.y min q.y
@@ -88,15 +73,13 @@
       ds.foreach(d => path.lineTo(d.x, d.y))
       path.lineTo(q.x, q.y)
 
-      if (visualizer.show_dummies)
-        ds.foreach(Dummy.paint(gfx, visualizer, _))
+      if (visualizer.show_dummies) ds.foreach(paint_dummy(gfx, visualizer, _))
 
       gfx.setStroke(default_stroke)
       gfx.setColor(visualizer.edge_color(edge))
       gfx.draw(path)
 
-      if (visualizer.arrow_heads)
-        Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
+      if (visualizer.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
     }
   }
 
@@ -106,8 +89,8 @@
 
     def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
     {
-      val p = visualizer.layout.get_vertex(Layout.Node(edge._1))
-      val q = visualizer.layout.get_vertex(Layout.Node(edge._2))
+      val p = visualizer.layout.get_node(edge._1)
+      val q = visualizer.layout.get_node(edge._2)
       val ds =
       {
         val a = p.y min q.y
@@ -142,15 +125,13 @@
           q.x - slack * dx2, q.y - slack * dy2,
           q.x, q.y)
 
-        if (visualizer.show_dummies)
-          ds.foreach(Dummy.paint(gfx, visualizer, _))
+        if (visualizer.show_dummies) ds.foreach(paint_dummy(gfx, visualizer, _))
 
         gfx.setStroke(default_stroke)
         gfx.setColor(visualizer.edge_color(edge))
         gfx.draw(path)
 
-        if (visualizer.arrow_heads)
-          Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
+        if (visualizer.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
       }
     }
   }

--- a/src/Tools/Graphview/visualizer.scala	Sat Jan 17 16:40:10 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sat Jan 17 22:20:57 2015 +0100
@@ -34,12 +34,12 @@
 
   def find_node(at: Point2D): Option[Graph_Display.Node] =
     layout.output_graph.iterator.collectFirst({
-      case (Layout.Node(node), _) if Shapes.Node.shape(visualizer, node).contains(at) => node
+      case (Layout.Node(node), (info, _)) if Shapes.shape(info).contains(at) => node
     })
 
   def find_dummy(at: Point2D): Option[Layout.Dummy] =
     layout.output_graph.iterator.collectFirst({
-      case (dummy: Layout.Dummy, (d, _)) if Shapes.Dummy.shape(visualizer, d).contains(at) => dummy
+      case (dummy: Layout.Dummy, (info, _)) if Shapes.shape(info).contains(at) => dummy
     })
 
   def bounding_box(): Rectangle2D.Double =
@@ -48,19 +48,17 @@
     var y0 = 0.0
     var x1 = 0.0
     var y1 = 0.0
-    ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++
-     (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))).
-       foreach(rect => {
-          x0 = x0 min rect.getMinX
-          y0 = y0 min rect.getMinY
-          x1 = x1 max rect.getMaxX
-          y1 = y1 max rect.getMaxY
-        })
-    val gap = metrics.gap
-    x0 = (x0 - gap).floor
-    y0 = (y0 - gap).floor
-    x1 = (x1 + gap).ceil
-    y1 = (y1 + gap).ceil
+    for ((_, (info, _)) <- layout.output_graph.iterator) {
+      val rect = Shapes.shape(info)
+      x0 = x0 min rect.getMinX
+      y0 = y0 min rect.getMinY
+      x1 = x1 max rect.getMaxX
+      y1 = y1 max rect.getMaxY
+    }
+    x0 = (x0 - metrics.gap).floor
+    y0 = (y0 - metrics.gap).floor
+    x1 = (x1 + metrics.gap).ceil
+    y1 = (y1 + metrics.gap).ceil
     new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
   }
 
@@ -69,8 +67,17 @@
     val metrics = Metrics(make_font())
     val visible_graph = model.make_visible_graph()
 
+    def node_text(node: Graph_Display.Node, content: XML.Body): String =
+      if (show_content) {
+        val s =
+          XML.content(Pretty.formatted(
+            content, options.int("graphview_content_margin").toDouble, metrics.Pretty_Metric))
+        if (s.nonEmpty) s else node.toString
+      }
+      else node.toString
+
     // FIXME avoid expensive operation on GUI thread
-    _layout = Layout.make(options, metrics, visible_graph)
+    _layout = Layout.make(options, metrics, node_text _, visible_graph)
   }
 
 
@@ -101,7 +108,8 @@
   /* rendering parameters */
 
   // owned by GUI thread
-  var arrow_heads = false
+  var show_content = false
+  var show_arrow_heads = false
   var show_dummies = false
 
   object Colors
@@ -130,7 +138,7 @@
     for (edge <- visible_graph.edges_iterator)
       Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge)
     for (node <- visible_graph.keys_iterator)
-      Shapes.Node.paint(gfx, visualizer, node)
+      Shapes.paint_node(gfx, visualizer, node)
   }
 
   object Selection