1/* Title: Tools/Graphview/mutator_dialog.scala 2 Author: Markus Kaiser, TU Muenchen 3 Author: Makarius 4 5Mutator selection and configuration dialog. 6*/ 7 8package isabelle.graphview 9 10 11import isabelle._ 12 13import java.awt.Color 14import java.awt.FocusTraversalPolicy 15import javax.swing.JColorChooser 16import javax.swing.border.EmptyBorder 17import scala.swing.{Dialog, Button, BoxPanel, Swing, Orientation, ComboBox, Action, 18 Dimension, BorderPanel, ScrollPane, Label, CheckBox, Alignment, Component, TextField} 19import scala.swing.event.ValueChanged 20 21 22class 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}