src/Tools/Graphview/mutator_dialog.scala
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 59459 985fc55e9f27
permissions -rw-r--r--
more strict AFP properties;
wenzelm@59202
     1
/*  Title:      Tools/Graphview/mutator_dialog.scala
markus@49557
     2
    Author:     Markus Kaiser, TU Muenchen
wenzelm@59240
     3
    Author:     Makarius
markus@49557
     4
markus@49557
     5
Mutator selection and configuration dialog.
markus@49557
     6
*/
markus@49557
     7
markus@49557
     8
package isabelle.graphview
markus@49557
     9
wenzelm@55618
    10
wenzelm@49558
    11
import isabelle._
markus@49557
    12
markus@49557
    13
import java.awt.Color
markus@49557
    14
import java.awt.FocusTraversalPolicy
markus@49557
    15
import javax.swing.JColorChooser
markus@49557
    16
import javax.swing.border.EmptyBorder
wenzelm@59222
    17
import scala.swing.{Dialog, Button, BoxPanel, Swing, Orientation, ComboBox, Action,
wenzelm@59222
    18
  Dimension, BorderPanel, ScrollPane, Label, CheckBox, Alignment, Component, TextField}
markus@49557
    19
import scala.swing.event.ValueChanged
markus@49557
    20
markus@49557
    21
markus@49557
    22
class Mutator_Dialog(
wenzelm@59459
    23
    graphview: Graphview,
wenzelm@50472
    24
    container: Mutator_Container,
wenzelm@50472
    25
    caption: String,
wenzelm@49733
    26
    reverse_caption: String = "Inverse",
wenzelm@49733
    27
    show_color_chooser: Boolean = true)
wenzelm@49733
    28
  extends Dialog
markus@49557
    29
{
markus@49557
    30
  title = caption
wenzelm@59218
    31
markus@49557
    32
  private var _panels: List[Mutator_Panel] = Nil
markus@49557
    33
  private def panels = _panels
wenzelm@59218
    34
  private def panels_=(panels: List[Mutator_Panel])
wenzelm@59218
    35
  {
markus@49557
    36
    _panels = panels
wenzelm@59222
    37
    paint_panels()
markus@49557
    38
  }
markus@49557
    39
wenzelm@59218
    40
  container.events +=
wenzelm@59218
    41
  {
wenzelm@59222
    42
    case Mutator_Event.Add(m) => add_panel(new Mutator_Panel(m))
wenzelm@59221
    43
    case Mutator_Event.New_List(ms) => panels = get_panels(ms)
markus@49557
    44
  }
markus@49557
    45
wenzelm@59218
    46
  override def open()
wenzelm@59218
    47
  {
wenzelm@59221
    48
    if (!visible) panels = get_panels(container())
markus@49557
    49
    super.open
markus@49557
    50
  }
markus@49557
    51
markus@49557
    52
  minimumSize = new Dimension(700, 200)
markus@49557
    53
  preferredSize = new Dimension(1000, 300)
wenzelm@59222
    54
  peer.setFocusTraversalPolicy(Focus_Traveral_Policy)
markus@49557
    55
wenzelm@59221
    56
  private def get_panels(m: List[Mutator.Info]): List[Mutator_Panel] =
wenzelm@59221
    57
    m.filter({ case Mutator.Info(_, _, Mutator.Identity()) => false case _ => true })
markus@49557
    58
    .map(m => new Mutator_Panel(m))
markus@49557
    59
wenzelm@59221
    60
  private def get_mutators(panels: List[Mutator_Panel]): List[Mutator.Info] =
wenzelm@59221
    61
    panels.map(panel => panel.get_mutator)
markus@49557
    62
wenzelm@59218
    63
  private def movePanelUp(m: Mutator_Panel) =
wenzelm@59218
    64
  {
wenzelm@59218
    65
    def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] =
wenzelm@59218
    66
      l match {
wenzelm@59218
    67
        case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs)
wenzelm@59218
    68
        case _ => l
wenzelm@59218
    69
      }
markus@49557
    70
markus@49557
    71
    panels = moveUp(panels)
markus@49557
    72
  }
markus@49557
    73
wenzelm@59218
    74
  private def movePanelDown(m: Mutator_Panel) =
wenzelm@59218
    75
  {
wenzelm@59218
    76
    def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] =
wenzelm@59218
    77
      l match {
wenzelm@59218
    78
        case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs)
wenzelm@59218
    79
        case _ => l
wenzelm@59218
    80
      }
markus@49557
    81
markus@49557
    82
    panels = moveDown(panels)
markus@49557
    83
  }
markus@49557
    84
wenzelm@59218
    85
  private def removePanel(m: Mutator_Panel)
wenzelm@59218
    86
  {
markus@49557
    87
    panels = panels.filter(_ != m).toList
markus@49557
    88
  }
markus@49557
    89
wenzelm@59222
    90
  private def add_panel(m: Mutator_Panel)
wenzelm@59218
    91
  {
markus@49557
    92
    panels = panels ::: List(m)
markus@49557
    93
  }
markus@49557
    94
wenzelm@59222
    95
  def paint_panels()
wenzelm@59218
    96
  {
wenzelm@59222
    97
    Focus_Traveral_Policy.clear
wenzelm@59222
    98
    filter_panel.contents.clear
markus@49557
    99
    panels.map(x => {
wenzelm@59222
   100
        filter_panel.contents += x
wenzelm@59222
   101
        Focus_Traveral_Policy.addAll(x.focusList)
markus@49557
   102
      })
wenzelm@59222
   103
    filter_panel.contents += Swing.VGlue
markus@49557
   104
wenzelm@59222
   105
    Focus_Traveral_Policy.add(mutator_box.peer.asInstanceOf[java.awt.Component])
wenzelm@59222
   106
    Focus_Traveral_Policy.add(add_button.peer)
wenzelm@59222
   107
    Focus_Traveral_Policy.add(apply_button.peer)
wenzelm@59222
   108
    Focus_Traveral_Policy.add(cancel_button.peer)
wenzelm@59222
   109
    filter_panel.revalidate
wenzelm@59222
   110
    filter_panel.repaint
markus@49557
   111
  }
markus@49557
   112
wenzelm@59222
   113
  val filter_panel = new BoxPanel(Orientation.Vertical) {}
markus@49557
   114
wenzelm@59221
   115
  private val mutator_box = new ComboBox[Mutator](container.available)
markus@49557
   116
wenzelm@59222
   117
  private val add_button = new Button {
markus@49557
   118
    action = Action("Add") {
wenzelm@59222
   119
      add_panel(
wenzelm@59459
   120
        new Mutator_Panel(Mutator.Info(true, graphview.Colors.next, mutator_box.selection.item)))
markus@49557
   121
    }
markus@49557
   122
  }
markus@49557
   123
wenzelm@59221
   124
  private val apply_button = new Button {
wenzelm@59221
   125
    action = Action("Apply") { container(get_mutators(panels)) }
markus@49557
   126
  }
markus@49557
   127
wenzelm@59221
   128
  private val reset_button = new Button {
wenzelm@59221
   129
    action = Action("Reset") { panels = get_panels(container()) }
markus@49557
   130
  }
markus@49557
   131
wenzelm@59221
   132
  private val cancel_button = new Button {
wenzelm@59221
   133
    action = Action("Close") { close }
wenzelm@59218
   134
  }
wenzelm@59221
   135
  defaultButton = cancel_button
markus@49557
   136
markus@49557
   137
  private val botPanel = new BoxPanel(Orientation.Horizontal) {
markus@49557
   138
    border = new EmptyBorder(10, 0, 0, 0)
markus@49557
   139
wenzelm@59221
   140
    contents += mutator_box
markus@49557
   141
    contents += Swing.RigidBox(new Dimension(10, 0))
wenzelm@59221
   142
    contents += add_button
markus@49557
   143
markus@49557
   144
    contents += Swing.HGlue
markus@49557
   145
    contents += Swing.RigidBox(new Dimension(30, 0))
wenzelm@59221
   146
    contents += apply_button
markus@49557
   147
markus@49557
   148
    contents += Swing.RigidBox(new Dimension(5, 0))
wenzelm@59221
   149
    contents += reset_button
markus@49557
   150
markus@49557
   151
    contents += Swing.RigidBox(new Dimension(5, 0))
wenzelm@59221
   152
    contents += cancel_button
markus@49557
   153
  }
wenzelm@59218
   154
markus@49557
   155
  contents = new BorderPanel {
markus@49557
   156
    border = new EmptyBorder(5, 5, 5, 5)
markus@49557
   157
wenzelm@59391
   158
    layout(new ScrollPane(filter_panel)) = BorderPanel.Position.Center
wenzelm@59391
   159
    layout(botPanel) = BorderPanel.Position.South
markus@49557
   160
  }
markus@49557
   161
wenzelm@59221
   162
  private class Mutator_Panel(initials: Mutator.Info)
wenzelm@50472
   163
    extends BoxPanel(Orientation.Horizontal)
markus@49557
   164
  {
wenzelm@59229
   165
    private val inputs: List[(String, Input)] = get_inputs()
wenzelm@50467
   166
    var focusList = List.empty[java.awt.Component]
wenzelm@59229
   167
    private val enabledBox = new Check_Box_Input("Enabled", initials.enabled)
markus@49557
   168
markus@49557
   169
    border = new EmptyBorder(5, 5, 5, 5)
markus@49557
   170
    maximumSize = new Dimension(Integer.MAX_VALUE, 30)
wenzelm@59221
   171
    background = initials.color
markus@49557
   172
wenzelm@59221
   173
    contents += new Label(initials.mutator.name) {
markus@49557
   174
      preferredSize = new Dimension(175, 20)
markus@49557
   175
      horizontalAlignment = Alignment.Left
wenzelm@59221
   176
      if (initials.mutator.description != "") tooltip = initials.mutator.description
markus@49557
   177
    }
markus@49557
   178
    contents += Swing.RigidBox(new Dimension(10, 0))
markus@49557
   179
    contents += enabledBox
markus@49557
   180
    contents += Swing.RigidBox(new Dimension(5, 0))
markus@49557
   181
    focusList = enabledBox.peer :: focusList
wenzelm@59218
   182
    inputs.map(_ match {
wenzelm@59218
   183
      case (n, c) =>
wenzelm@59218
   184
        contents += Swing.RigidBox(new Dimension(10, 0))
markus@49557
   185
        if (n != "") {
markus@49557
   186
          contents += new Label(n)
markus@49557
   187
          contents += Swing.RigidBox(new Dimension(5, 0))
markus@49557
   188
        }
markus@49557
   189
        contents += c.asInstanceOf[Component]
wenzelm@59218
   190
markus@49557
   191
        focusList = c.asInstanceOf[Component].peer :: focusList
markus@49557
   192
      case _ =>
markus@49557
   193
    })
markus@49557
   194
markus@49557
   195
    {
markus@49557
   196
      val t = this
markus@49557
   197
      contents += Swing.HGlue
markus@49557
   198
      contents += Swing.RigidBox(new Dimension(10, 0))
markus@49557
   199
markus@49557
   200
      if (show_color_chooser) {
markus@49557
   201
        contents += new Button {
markus@49557
   202
          maximumSize = new Dimension(20, 20)
markus@49557
   203
markus@49557
   204
          action = Action("Color") {
markus@49557
   205
            t.background =
markus@49557
   206
              JColorChooser.showDialog(t.peer, "Choose new Color", t.background)
markus@49557
   207
          }
markus@49557
   208
markus@49557
   209
          focusList = this.peer :: focusList
markus@49557
   210
        }
markus@49557
   211
        contents += Swing.RigidBox(new Dimension(2, 0))
markus@49557
   212
      }
markus@49557
   213
markus@49557
   214
      contents += new Button {
markus@49557
   215
        maximumSize = new Dimension(20, 20)
markus@49557
   216
markus@49557
   217
        action = Action("Up") {
markus@49557
   218
          movePanelUp(t)
markus@49557
   219
        }
markus@49557
   220
markus@49557
   221
        focusList = this.peer :: focusList
markus@49557
   222
      }
markus@49557
   223
      contents += Swing.RigidBox(new Dimension(2, 0))
markus@49557
   224
      contents += new Button {
markus@49557
   225
        maximumSize = new Dimension(20, 20)
markus@49557
   226
markus@49557
   227
        action = Action("Down") {
markus@49557
   228
          movePanelDown(t)
markus@49557
   229
        }
markus@49557
   230
markus@49557
   231
        focusList = this.peer :: focusList
markus@49557
   232
      }
markus@49557
   233
      contents += Swing.RigidBox(new Dimension(2, 0))
markus@49557
   234
      contents += new Button {
markus@49557
   235
        maximumSize = new Dimension(20, 20)
markus@49557
   236
markus@49557
   237
        action = Action("Del") {
markus@49557
   238
          removePanel(t)
markus@49557
   239
        }
markus@49557
   240
markus@49557
   241
        focusList = this.peer :: focusList
markus@49557
   242
      }
markus@49557
   243
    }
markus@49557
   244
markus@49557
   245
    focusList = focusList.reverse
markus@49557
   246
wenzelm@59221
   247
    def get_mutator: Mutator.Info =
wenzelm@59218
   248
    {
wenzelm@59459
   249
      val model = graphview.model
wenzelm@59221
   250
      val m =
wenzelm@59221
   251
        initials.mutator match {
wenzelm@59221
   252
          case Mutator.Identity() =>
wenzelm@59221
   253
            Mutator.Identity()
wenzelm@59221
   254
          case Mutator.Node_Expression(r, _, _, _) =>
wenzelm@59229
   255
            val r1 = inputs(2)._2.string
wenzelm@59221
   256
            Mutator.Node_Expression(
wenzelm@59224
   257
              if (Library.make_regex(r1).isDefined) r1 else r,
wenzelm@59229
   258
              inputs(3)._2.bool,
wenzelm@59221
   259
              // "Parents" means "Show parents" or "Matching Children"
wenzelm@59229
   260
              inputs(1)._2.bool,
wenzelm@59229
   261
              inputs(0)._2.bool)
wenzelm@59221
   262
          case Mutator.Node_List(_, _, _, _) =>
wenzelm@59221
   263
            Mutator.Node_List(
wenzelm@59245
   264
              for {
wenzelm@59245
   265
                ident <- space_explode(',', inputs(2)._2.string)
wenzelm@59245
   266
                node <- model.find_node(ident)
wenzelm@59245
   267
              } yield node,
wenzelm@59229
   268
              inputs(3)._2.bool,
wenzelm@59221
   269
              // "Parents" means "Show parents" or "Matching Children"
wenzelm@59229
   270
              inputs(1)._2.bool,
wenzelm@59229
   271
              inputs(0)._2.bool)
wenzelm@59246
   272
          case Mutator.Edge_Endpoints(_) =>
wenzelm@59245
   273
            (model.find_node(inputs(0)._2.string), model.find_node(inputs(1)._2.string)) match {
wenzelm@59245
   274
              case (Some(node1), Some(node2)) =>
wenzelm@59246
   275
                Mutator.Edge_Endpoints((node1, node2))
wenzelm@59245
   276
              case _ =>
wenzelm@59245
   277
                Mutator.Identity()
wenzelm@59245
   278
            }
wenzelm@59221
   279
          case Mutator.Add_Node_Expression(r) =>
wenzelm@59229
   280
            val r1 = inputs(0)._2.string
wenzelm@59224
   281
            Mutator.Add_Node_Expression(if (Library.make_regex(r1).isDefined) r1 else r)
wenzelm@59221
   282
          case Mutator.Add_Transitive_Closure(_, _) =>
wenzelm@59221
   283
            Mutator.Add_Transitive_Closure(
wenzelm@59229
   284
              inputs(0)._2.bool,
wenzelm@59229
   285
              inputs(1)._2.bool)
wenzelm@59221
   286
          case _ =>
wenzelm@59221
   287
            Mutator.Identity()
wenzelm@59221
   288
        }
wenzelm@59218
   289
wenzelm@59221
   290
      Mutator.Info(enabledBox.selected, background, m)
markus@49557
   291
    }
wenzelm@59218
   292
wenzelm@59229
   293
    private def get_inputs(): List[(String, Input)] =
wenzelm@59221
   294
      initials.mutator match {
wenzelm@59221
   295
        case Mutator.Node_Expression(regex, reverse, check_parents, check_children) =>
wenzelm@59218
   296
          List(
wenzelm@59229
   297
            ("", new Check_Box_Input("Parents", check_children)),
wenzelm@59229
   298
            ("", new Check_Box_Input("Children", check_parents)),
wenzelm@59229
   299
            ("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)),
wenzelm@59229
   300
            ("", new Check_Box_Input(reverse_caption, reverse)))
wenzelm@59221
   301
        case Mutator.Node_List(list, reverse, check_parents, check_children) =>
wenzelm@59218
   302
          List(
wenzelm@59229
   303
            ("", new Check_Box_Input("Parents", check_children)),
wenzelm@59229
   304
            ("", new Check_Box_Input("Children", check_parents)),
wenzelm@59245
   305
            ("Names", new Text_Field_Input(list.map(_.ident).mkString(","))),
wenzelm@59229
   306
            ("", new Check_Box_Input(reverse_caption, reverse)))
wenzelm@59246
   307
        case Mutator.Edge_Endpoints((source, dest)) =>
wenzelm@59218
   308
          List(
wenzelm@59245
   309
            ("Source", new Text_Field_Input(source.ident)),
wenzelm@59245
   310
            ("Destination", new Text_Field_Input(dest.ident)))
wenzelm@59221
   311
        case Mutator.Add_Node_Expression(regex) =>
wenzelm@59229
   312
          List(("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)))
wenzelm@59221
   313
        case Mutator.Add_Transitive_Closure(parents, children) =>
wenzelm@59218
   314
          List(
wenzelm@59229
   315
            ("", new Check_Box_Input("Parents", parents)),
wenzelm@59229
   316
            ("", new Check_Box_Input("Children", children)))
wenzelm@59218
   317
        case _ => Nil
wenzelm@59218
   318
      }
markus@49557
   319
  }
markus@49557
   320
wenzelm@59229
   321
  private trait Input
markus@49557
   322
  {
wenzelm@59229
   323
    def string: String
wenzelm@59229
   324
    def bool: Boolean
markus@49557
   325
  }
markus@49557
   326
wenzelm@59229
   327
  private class Text_Field_Input(txt: String, check: String => Boolean = (_: String) => true)
wenzelm@59229
   328
    extends TextField(txt) with Input
markus@49557
   329
  {
markus@49557
   330
    preferredSize = new Dimension(125, 18)
markus@49557
   331
wenzelm@59228
   332
    private val default_foreground = foreground
wenzelm@59218
   333
    reactions +=
wenzelm@59218
   334
    {
markus@49557
   335
      case ValueChanged(_) =>
wenzelm@59459
   336
        foreground = if (check(text)) default_foreground else graphview.error_color
markus@49557
   337
    }
markus@49557
   338
wenzelm@59229
   339
    def string = text
wenzelm@59229
   340
    def bool = true
markus@49557
   341
  }
markus@49557
   342
wenzelm@59229
   343
  private class Check_Box_Input(txt: String, s: Boolean) extends CheckBox(txt) with Input
markus@49557
   344
  {
markus@49557
   345
    selected = s
markus@49557
   346
wenzelm@59229
   347
    def string = ""
wenzelm@59229
   348
    def bool = selected
markus@49557
   349
  }
markus@49557
   350
wenzelm@59222
   351
  private object Focus_Traveral_Policy extends FocusTraversalPolicy
markus@49557
   352
  {
wenzelm@59222
   353
    private var items = Vector.empty[java.awt.Component]
markus@49557
   354
wenzelm@59218
   355
    def add(c: java.awt.Component) { items = items :+ c }
wenzelm@59218
   356
    def addAll(cs: TraversableOnce[java.awt.Component]) { items = items ++ cs }
wenzelm@59222
   357
    def clear() { items = Vector.empty }
markus@49557
   358
wenzelm@59218
   359
    def getComponentAfter(root: java.awt.Container, c: java.awt.Component): java.awt.Component =
wenzelm@59218
   360
    {
markus@49557
   361
      val i = items.indexOf(c)
wenzelm@59218
   362
      if (i < 0) getDefaultComponent(root)
wenzelm@59218
   363
      else items((i + 1) % items.length)
markus@49557
   364
    }
markus@49557
   365
wenzelm@59218
   366
    def getComponentBefore(root: java.awt.Container, c: java.awt.Component): java.awt.Component =
wenzelm@59218
   367
    {
markus@49557
   368
      val i = items.indexOf(c)
wenzelm@59218
   369
      if (i < 0) getDefaultComponent(root)
wenzelm@59218
   370
      else items((i - 1) % items.length)
markus@49557
   371
    }
markus@49557
   372
wenzelm@59218
   373
    def getFirstComponent(root: java.awt.Container): java.awt.Component =
wenzelm@59218
   374
      if (items.length > 0) items(0) else null
markus@49557
   375
wenzelm@59218
   376
    def getDefaultComponent(root: java.awt.Container): java.awt.Component =
wenzelm@59218
   377
      getFirstComponent(root)
markus@49557
   378
wenzelm@59218
   379
    def getLastComponent(root: java.awt.Container): java.awt.Component =
wenzelm@59218
   380
      if (items.length > 0) items.last else null
markus@49557
   381
  }
markus@49557
   382
}