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