src/Tools/Graphview/graphview.scala
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (19 months ago)
changeset 67835 c8e4ee2b5482
parent 67547 aefe7a7b330a
permissions -rw-r--r--
tuned imports;
     1 /*  Title:      Tools/Graphview/graphview.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3     Author:     Makarius
     4 
     5 Graphview visualization parameters and GUI state.
     6 */
     7 
     8 package isabelle.graphview
     9 
    10 
    11 import isabelle._
    12 
    13 import java.awt.{Font, Color, Shape, Graphics2D}
    14 import java.awt.geom.{Point2D, Rectangle2D}
    15 import javax.swing.JComponent
    16 
    17 
    18 abstract class Graphview(full_graph: Graph_Display.Graph)
    19 {
    20   graphview =>
    21 
    22 
    23   def options: Options
    24 
    25   val model = new Model(full_graph)
    26 
    27 
    28   /* layout state */
    29 
    30   // owned by GUI thread
    31   private var _layout: Layout = Layout.empty
    32   def layout: Layout = _layout
    33 
    34   def metrics: Metrics = layout.metrics
    35   def visible_graph: Graph_Display.Graph = layout.input_graph
    36 
    37   def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit =
    38     _layout = _layout.translate_vertex(v, dx, dy)
    39 
    40   def find_node(at: Point2D): Option[Graph_Display.Node] =
    41     layout.output_graph.iterator.collectFirst({
    42       case (Layout.Node(node), (info, _)) if Shapes.shape(info).contains(at) => node
    43     })
    44 
    45   def find_dummy(at: Point2D): Option[Layout.Dummy] =
    46     layout.output_graph.iterator.collectFirst({
    47       case (dummy: Layout.Dummy, (info, _)) if Shapes.shape(info).contains(at) => dummy
    48     })
    49 
    50   def bounding_box(): Rectangle2D.Double =
    51   {
    52     var x0 = 0.0
    53     var y0 = 0.0
    54     var x1 = 0.0
    55     var y1 = 0.0
    56     for ((_, (info, _)) <- layout.output_graph.iterator) {
    57       val rect = Shapes.shape(info)
    58       x0 = x0 min rect.getMinX
    59       y0 = y0 min rect.getMinY
    60       x1 = x1 max rect.getMaxX
    61       y1 = y1 max rect.getMaxY
    62     }
    63     x0 = (x0 - metrics.gap).floor
    64     y0 = (y0 - metrics.gap).floor
    65     x1 = (x1 + metrics.gap).ceil
    66     y1 = (y1 + metrics.gap).ceil
    67     new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
    68   }
    69 
    70   def update_layout()
    71   {
    72     val metrics = Metrics(make_font())
    73     val visible_graph = model.make_visible_graph()
    74 
    75     def node_text(node: Graph_Display.Node, content: XML.Body): String =
    76       if (show_content) {
    77         val s =
    78           XML.content(Pretty.formatted(content,
    79             margin = options.int("graphview_content_margin").toDouble,
    80             metric = metrics.Pretty_Metric))
    81         if (s.nonEmpty) s else node.toString
    82       }
    83       else node.toString
    84 
    85     _layout = Layout.make(options, metrics, node_text _, visible_graph)
    86   }
    87 
    88 
    89   /* tooltips */
    90 
    91   def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
    92 
    93 
    94   /* main colors */
    95 
    96   def foreground_color: Color = Color.BLACK
    97   def background_color: Color = Color.WHITE
    98   def selection_color: Color = new Color(204, 204, 255)
    99   def highlight_color: Color = new Color(255, 255, 224)
   100   def error_color: Color = Color.RED
   101   def dummy_color: Color = Color.GRAY
   102 
   103 
   104   /* font rendering information */
   105 
   106   def make_font(): Font =
   107   {
   108     val family = options.string("graphview_font_family")
   109     val size = options.int("graphview_font_size")
   110     new Font(family, Font.PLAIN, size)
   111   }
   112 
   113 
   114   /* rendering parameters */
   115 
   116   // owned by GUI thread
   117   var show_content = false
   118   var show_arrow_heads = false
   119   var show_dummies = false
   120   var editor_style = false
   121 
   122   object Colors
   123   {
   124     private val filter_colors = List(
   125       new Color(0xD9, 0xF2, 0xE2), // blue
   126       new Color(0xFF, 0xE7, 0xD8), // orange
   127       new Color(0xFF, 0xFF, 0xE5), // yellow
   128       new Color(0xDE, 0xCE, 0xFF), // lilac
   129       new Color(0xCC, 0xEB, 0xFF), // turquoise
   130       new Color(0xFF, 0xE5, 0xE5), // red
   131       new Color(0xE5, 0xE5, 0xD9)  // green
   132     )
   133 
   134     private var curr : Int = -1
   135     def next(): Color =
   136     {
   137       curr = (curr + 1) % filter_colors.length
   138       filter_colors(curr)
   139     }
   140   }
   141 
   142   def paint(gfx: Graphics2D)
   143   {
   144     gfx.setRenderingHints(Metrics.rendering_hints)
   145 
   146     for (node <- graphview.current_node)
   147       Shapes.highlight_node(gfx, graphview, node)
   148 
   149     for (edge <- visible_graph.edges_iterator)
   150       Shapes.Cardinal_Spline_Edge.paint(gfx, graphview, edge)
   151 
   152     for (node <- visible_graph.keys_iterator)
   153       Shapes.paint_node(gfx, graphview, node)
   154   }
   155 
   156   var current_node: Option[Graph_Display.Node] = None
   157 
   158   object Selection
   159   {
   160     private val state = Synchronized[List[Graph_Display.Node]](Nil)
   161 
   162     def get(): List[Graph_Display.Node] = state.value
   163     def contains(node: Graph_Display.Node): Boolean = get().contains(node)
   164 
   165     def add(node: Graph_Display.Node): Unit = state.change(node :: _)
   166     def clear(): Unit = state.change(_ => Nil)
   167   }
   168 
   169   sealed case class Node_Color(border: Color, background: Color, foreground: Color)
   170 
   171   def node_color(node: Graph_Display.Node): Node_Color =
   172     if (Selection.contains(node))
   173       Node_Color(foreground_color, selection_color, foreground_color)
   174     else if (current_node == Some(node))
   175       Node_Color(foreground_color, highlight_color, foreground_color)
   176     else
   177       Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
   178 
   179   def edge_color(edge: Graph_Display.Edge, downwards: Boolean): Color =
   180     if (downwards || show_arrow_heads) foreground_color
   181     else error_color
   182 }