src/Tools/Graphview/shapes.scala
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (19 months ago)
changeset 67835 c8e4ee2b5482
parent 62812 ce22e5c3d4ce
permissions -rw-r--r--
tuned imports;
     1 /*  Title:      Tools/Graphview/shapes.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3     Author:     Makarius
     4 
     5 Drawable shapes.
     6 */
     7 
     8 package isabelle.graphview
     9 
    10 
    11 import isabelle._
    12 
    13 import java.awt.{BasicStroke, Graphics2D, Shape}
    14 import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D,
    15   RoundRectangle2D, PathIterator}
    16 
    17 
    18 object Shapes
    19 {
    20   private val default_stroke =
    21     new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
    22 
    23   def shape(info: Layout.Info): Rectangle2D.Double =
    24     new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height)
    25 
    26   def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node)
    27   {
    28     val metrics = graphview.metrics
    29     val extra = metrics.char_width
    30     val info = graphview.layout.get_node(node)
    31 
    32     gfx.setColor(graphview.highlight_color)
    33     gfx.fill(new Rectangle2D.Double(
    34       info.x - info.width2 - extra,
    35       info.y - info.height2 - extra,
    36       info.width + 2 * extra,
    37       info.height + 2 * extra))
    38   }
    39 
    40   def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node)
    41   {
    42     val metrics = graphview.metrics
    43     val info = graphview.layout.get_node(node)
    44     val c = graphview.node_color(node)
    45     val s = shape(info)
    46 
    47     gfx.setColor(c.background)
    48     gfx.fill(s)
    49 
    50     gfx.setColor(c.border)
    51     gfx.setStroke(default_stroke)
    52     gfx.draw(s)
    53 
    54     gfx.setColor(c.foreground)
    55     gfx.setFont(metrics.font)
    56 
    57     val text_width =
    58       (0.0 /: info.lines) { case (w, line) => w max metrics.string_bounds(line).getWidth }
    59     val text_height =
    60       (info.lines.length max 1) * metrics.height.ceil
    61     val x = (s.getCenterX - text_width / 2).round.toInt
    62     var y = (s.getCenterY - text_height / 2 + metrics.ascent).round.toInt
    63     for (line <- info.lines) {
    64       gfx.drawString(Word.bidi_override(line), x, y)
    65       y += metrics.height.ceil.toInt
    66     }
    67   }
    68 
    69   def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info)
    70   {
    71     gfx.setStroke(default_stroke)
    72     gfx.setColor(graphview.dummy_color)
    73     gfx.draw(shape(info))
    74   }
    75 
    76   object Straight_Edge
    77   {
    78     def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge)
    79     {
    80       val p = graphview.layout.get_node(edge._1)
    81       val q = graphview.layout.get_node(edge._2)
    82       val ds =
    83       {
    84         val a = p.y min q.y
    85         val b = p.y max q.y
    86         graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
    87       }
    88       val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
    89 
    90       path.moveTo(p.x, p.y)
    91       ds.foreach(d => path.lineTo(d.x, d.y))
    92       path.lineTo(q.x, q.y)
    93 
    94       if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _))
    95 
    96       gfx.setStroke(default_stroke)
    97       gfx.setColor(graphview.edge_color(edge, p.y < q.y))
    98       gfx.draw(path)
    99 
   100       if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
   101     }
   102   }
   103 
   104   object Cardinal_Spline_Edge
   105   {
   106     private val slack = 0.1
   107 
   108     def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge)
   109     {
   110       val p = graphview.layout.get_node(edge._1)
   111       val q = graphview.layout.get_node(edge._2)
   112       val ds =
   113       {
   114         val a = p.y min q.y
   115         val b = p.y max q.y
   116         graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
   117       }
   118 
   119       if (ds.isEmpty) Straight_Edge.paint(gfx, graphview, edge)
   120       else {
   121         val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
   122         path.moveTo(p.x, p.y)
   123 
   124         val coords = p :: ds ::: List(q)
   125         val dx = coords(2).x - coords(0).x
   126         val dy = coords(2).y - coords(0).y
   127 
   128         val (dx2, dy2) =
   129           ((dx, dy) /: coords.sliding(3)) {
   130             case ((dx, dy), List(l, m, r)) =>
   131               val dx2 = r.x - l.x
   132               val dy2 = r.y - l.y
   133               path.curveTo(
   134                 l.x + slack * dx, l.y + slack * dy,
   135                 m.x - slack * dx2, m.y - slack * dy2,
   136                 m.x, m.y)
   137               (dx2, dy2)
   138           }
   139 
   140         val l = ds.last
   141         path.curveTo(
   142           l.x + slack * dx2, l.y + slack * dy2,
   143           q.x - slack * dx2, q.y - slack * dy2,
   144           q.x, q.y)
   145 
   146         if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _))
   147 
   148         gfx.setStroke(default_stroke)
   149         gfx.setColor(graphview.edge_color(edge, p.y < q.y))
   150         gfx.draw(path)
   151 
   152         if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
   153       }
   154     }
   155   }
   156 
   157   object Arrow_Head
   158   {
   159     type Point = (Double, Double)
   160 
   161     private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] =
   162     {
   163       def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] =
   164       {
   165         val i = path.getPathIterator(null, 1.0)
   166         val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0)
   167         var p1 = (0.0, 0.0)
   168         var p2 = (0.0, 0.0)
   169         while (!i.isDone) {
   170           i.currentSegment(seg) match {
   171             case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1))
   172             case PathIterator.SEG_LINETO =>
   173               p1 = p2
   174               p2 = (seg(0), seg(1))
   175 
   176               if(shape.contains(seg(0), seg(1)))
   177                 return Some((p1, p2))
   178             case _ =>
   179           }
   180           i.next()
   181         }
   182         None
   183       }
   184 
   185       def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] =
   186       {
   187         val ((fx, fy), (tx, ty)) = line
   188         if (shape.contains(fx, fy) == shape.contains(tx, ty))
   189           None
   190         else {
   191           val (dx, dy) = (fx - tx, fy - ty)
   192           if ((dx * dx + dy * dy) < 1.0) {
   193             val at = AffineTransform.getTranslateInstance(fx, fy)
   194             at.rotate(- (math.atan2(dx, dy) + math.Pi / 2))
   195             Some(at)
   196           }
   197           else {
   198             val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0)
   199             if (shape.contains(fx, fy) == shape.contains(mx, my))
   200               binary_search(((mx, my), (tx, ty)), shape)
   201             else
   202               binary_search(((fx, fy), (mx, my)), shape)
   203           }
   204         }
   205       }
   206 
   207       intersecting_line(path, shape) match {
   208         case None => None
   209         case Some(line) => binary_search(line, shape)
   210       }
   211     }
   212 
   213     def paint(gfx: Graphics2D, path: GeneralPath, shape: Shape)
   214     {
   215       position(path, shape) match {
   216         case None =>
   217         case Some(at) =>
   218           val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3)
   219           arrow.moveTo(0, 0)
   220           arrow.lineTo(-10, 4)
   221           arrow.lineTo(-6, 0)
   222           arrow.lineTo(-10, -4)
   223           arrow.lineTo(0, 0)
   224           arrow.transform(at)
   225           gfx.fill(arrow)
   226       }
   227     }
   228   }
   229 }