Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: shapes.scala Sprache: Scala

Original von: Isabelle^©

/*  Title:      Tools/Graphview/shapes.scala
    Author:     Markus Kaiser, TU Muenchen
    Author:     Makarius

Drawable shapes.
*/

package isabelle.graphview

import isabelle._

import java.awt.{BasicStroke, Graphics2D, Shape}
import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D,
  RoundRectangle2D, PathIterator}

object Shapes
{
  private val default_stroke =
    new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)

  def shape(info: Layout.Info): Rectangle2D.Double =
    new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height)

  def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node)
  {
    val metrics = graphview.metrics
    val extra = metrics.char_width
    val info = graphview.layout.get_node(node)

    gfx.setColor(graphview.highlight_color)
    gfx.fill(new Rectangle2D.Double(
      info.x - info.width2 - extra,
      info.y - info.height2 - extra,
      info.width + 2 * extra,
      info.height + 2 * extra))
  }

  def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node)
  {
    val metrics = graphview.metrics
    val info = graphview.layout.get_node(node)
    val c = graphview.node_color(node)
    val s = shape(info)

    gfx.setColor(c.background)
    gfx.fill(s)

    gfx.setColor(c.border)
    gfx.setStroke(default_stroke)
    gfx.draw(s)

    gfx.setColor(c.foreground)
    gfx.setFont(metrics.font)

    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(Word.bidi_override(line), x, y)
      y += metrics.height.ceil.toInt
    }
  }

  def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info)
  {
    gfx.setStroke(default_stroke)
    gfx.setColor(graphview.dummy_color)
    gfx.draw(shape(info))
  }

  object Straight_Edge
  {
    def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge)
    {
      val p = graphview.layout.get_node(edge._1)
      val q = graphview.layout.get_node(edge._2)
      val ds =
      {
        val a = p.y min q.y
        val b = p.y max q.y
        graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
      }
      val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)

      path.moveTo(p.x, p.y)
      ds.foreach(d => path.lineTo(d.x, d.y))
      path.lineTo(q.x, q.y)

      if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _))

      gfx.setStroke(default_stroke)
      gfx.setColor(graphview.edge_color(edge, p.y < q.y))
      gfx.draw(path)

      if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
    }
  }

  object Cardinal_Spline_Edge
  {
    private val slack = 0.1

    def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge)
    {
      val p = graphview.layout.get_node(edge._1)
      val q = graphview.layout.get_node(edge._2)
      val ds =
      {
        val a = p.y min q.y
        val b = p.y max q.y
        graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
      }

      if (ds.isEmpty) Straight_Edge.paint(gfx, graphview, edge)
      else {
        val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
        path.moveTo(p.x, p.y)

        val coords = p :: ds ::: List(q)
        val dx = coords(2).x - coords(0).x
        val dy = coords(2).y - coords(0).y

        val (dx2, dy2) =
          ((dx, dy) /: coords.sliding(3)) {
            case ((dx, dy), List(l, m, r)) =>
              val dx2 = r.x - l.x
              val dy2 = r.y - l.y
              path.curveTo(
                l.x + slack * dx, l.y + slack * dy,
                m.x - slack * dx2, m.y - slack * dy2,
                m.x, m.y)
              (dx2, dy2)
          }

        val l = ds.last
        path.curveTo(
          l.x + slack * dx2, l.y + slack * dy2,
          q.x - slack * dx2, q.y - slack * dy2,
          q.x, q.y)

        if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _))

        gfx.setStroke(default_stroke)
        gfx.setColor(graphview.edge_color(edge, p.y < q.y))
        gfx.draw(path)

        if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
      }
    }
  }

  object Arrow_Head
  {
    type Point = (Double, Double)

    private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] =
    {
      def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] =
      {
        val i = path.getPathIterator(null, 1.0)
        val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0)
        var p1 = (0.0, 0.0)
        var p2 = (0.0, 0.0)
        while (!i.isDone) {
          i.currentSegment(seg) match {
            case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1))
            case PathIterator.SEG_LINETO =>
              p1 = p2
              p2 = (seg(0), seg(1))

              if(shape.contains(seg(0), seg(1)))
                return Some((p1, p2))
            case _ =>
          }
          i.next()
        }
        None
      }

      def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] =
      {
        val ((fx, fy), (tx, ty)) = line
        if (shape.contains(fx, fy) == shape.contains(tx, ty))
          None
        else {
          val (dx, dy) = (fx - tx, fy - ty)
          if ((dx * dx + dy * dy) < 1.0) {
            val at = AffineTransform.getTranslateInstance(fx, fy)
            at.rotate(- (math.atan2(dx, dy) + math.Pi / 2))
            Some(at)
          }
          else {
            val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0)
            if (shape.contains(fx, fy) == shape.contains(mx, my))
              binary_search(((mx, my), (tx, ty)), shape)
            else
              binary_search(((fx, fy), (mx, my)), shape)
          }
        }
      }

      intersecting_line(path, shape) match {
        case None => None
        case Some(line) => binary_search(line, shape)
      }
    }

    def paint(gfx: Graphics2D, path: GeneralPath, shape: Shape)
    {
      position(path, shape) match {
        case None =>
        case Some(at) =>
          val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3)
          arrow.moveTo(0, 0)
          arrow.lineTo(-10, 4)
          arrow.lineTo(-6, 0)
          arrow.lineTo(-10, -4)
          arrow.lineTo(0, 0)
          arrow.transform(at)
          gfx.fill(arrow)
      }
    }
  }
}

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.