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