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({ 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 }) 193 194 { 195 val t = this 196 contents += Swing.HGlue 197 contents += Swing.RigidBox(new Dimension(10, 0)) 198 199 if (show_color_chooser) { 200 contents += new Button { 201 maximumSize = new Dimension(20, 20) 202 203 action = Action("Color") { 204 t.background = 205 JColorChooser.showDialog(t.peer, "Choose new Color", t.background) 206 } 207 208 focusList = this.peer :: focusList 209 } 210 contents += Swing.RigidBox(new Dimension(2, 0)) 211 } 212 213 contents += new Button { 214 maximumSize = new Dimension(20, 20) 215 216 action = Action("Up") { 217 movePanelUp(t) 218 } 219 220 focusList = this.peer :: focusList 221 } 222 contents += Swing.RigidBox(new Dimension(2, 0)) 223 contents += new Button { 224 maximumSize = new Dimension(20, 20) 225 226 action = Action("Down") { 227 movePanelDown(t) 228 } 229 230 focusList = this.peer :: focusList 231 } 232 contents += Swing.RigidBox(new Dimension(2, 0)) 233 contents += new Button { 234 maximumSize = new Dimension(20, 20) 235 236 action = Action("Del") { 237 removePanel(t) 238 } 239 240 focusList = this.peer :: focusList 241 } 242 } 243 244 focusList = focusList.reverse 245 246 def get_mutator: Mutator.Info = 247 { 248 val model = graphview.model 249 val m = 250 initials.mutator match { 251 case Mutator.Identity() => 252 Mutator.Identity() 253 case Mutator.Node_Expression(r, _, _, _) => 254 val r1 = inputs(2)._2.string 255 Mutator.Node_Expression( 256 if (Library.make_regex(r1).isDefined) r1 else r, 257 inputs(3)._2.bool, 258 // "Parents" means "Show parents" or "Matching Children" 259 inputs(1)._2.bool, 260 inputs(0)._2.bool) 261 case Mutator.Node_List(_, _, _, _) => 262 Mutator.Node_List( 263 for { 264 ident <- space_explode(',', inputs(2)._2.string) 265 node <- model.find_node(ident) 266 } yield node, 267 inputs(3)._2.bool, 268 // "Parents" means "Show parents" or "Matching Children" 269 inputs(1)._2.bool, 270 inputs(0)._2.bool) 271 case Mutator.Edge_Endpoints(_) => 272 (model.find_node(inputs(0)._2.string), model.find_node(inputs(1)._2.string)) match { 273 case (Some(node1), Some(node2)) => 274 Mutator.Edge_Endpoints((node1, node2)) 275 case _ => 276 Mutator.Identity() 277 } 278 case Mutator.Add_Node_Expression(r) => 279 val r1 = inputs(0)._2.string 280 Mutator.Add_Node_Expression(if (Library.make_regex(r1).isDefined) r1 else r) 281 case Mutator.Add_Transitive_Closure(_, _) => 282 Mutator.Add_Transitive_Closure( 283 inputs(0)._2.bool, 284 inputs(1)._2.bool) 285 case _ => 286 Mutator.Identity() 287 } 288 289 Mutator.Info(enabledBox.selected, background, m) 290 } 291 292 private def get_inputs(): List[(String, Input)] = 293 initials.mutator match { 294 case Mutator.Node_Expression(regex, reverse, check_parents, check_children) => 295 List( 296 ("", new Check_Box_Input("Parents", check_children)), 297 ("", new Check_Box_Input("Children", check_parents)), 298 ("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)), 299 ("", new Check_Box_Input(reverse_caption, reverse))) 300 case Mutator.Node_List(list, reverse, check_parents, check_children) => 301 List( 302 ("", new Check_Box_Input("Parents", check_children)), 303 ("", new Check_Box_Input("Children", check_parents)), 304 ("Names", new Text_Field_Input(list.map(_.ident).mkString(","))), 305 ("", new Check_Box_Input(reverse_caption, reverse))) 306 case Mutator.Edge_Endpoints((source, dest)) => 307 List( 308 ("Source", new Text_Field_Input(source.ident)), 309 ("Destination", new Text_Field_Input(dest.ident))) 310 case Mutator.Add_Node_Expression(regex) => 311 List(("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined))) 312 case Mutator.Add_Transitive_Closure(parents, children) => 313 List( 314 ("", new Check_Box_Input("Parents", parents)), 315 ("", new Check_Box_Input("Children", children))) 316 case _ => Nil 317 } 318 } 319 320 private trait Input 321 { 322 def string: String 323 def bool: Boolean 324 } 325 326 private class Text_Field_Input(txt: String, check: String => Boolean = (_: String) => true) 327 extends TextField(txt) with Input 328 { 329 preferredSize = new Dimension(125, 18) 330 331 private val default_foreground = foreground 332 reactions += 333 { 334 case ValueChanged(_) => 335 foreground = if (check(text)) default_foreground else graphview.error_color 336 } 337 338 def string = text 339 def bool = true 340 } 341 342 private class Check_Box_Input(txt: String, s: Boolean) extends CheckBox(txt) with Input 343 { 344 selected = s 345 346 def string = "" 347 def bool = selected 348 } 349 350 private object Focus_Traveral_Policy extends FocusTraversalPolicy 351 { 352 private var items = Vector.empty[java.awt.Component] 353 354 def add(c: java.awt.Component) { items = items :+ c } 355 def addAll(cs: TraversableOnce[java.awt.Component]) { items = items ++ cs } 356 def clear() { items = Vector.empty } 357 358 def getComponentAfter(root: java.awt.Container, c: java.awt.Component): java.awt.Component = 359 { 360 val i = items.indexOf(c) 361 if (i < 0) getDefaultComponent(root) 362 else items((i + 1) % items.length) 363 } 364 365 def getComponentBefore(root: java.awt.Container, c: java.awt.Component): java.awt.Component = 366 { 367 val i = items.indexOf(c) 368 if (i < 0) getDefaultComponent(root) 369 else items((i - 1) % items.length) 370 } 371 372 def getFirstComponent(root: java.awt.Container): java.awt.Component = 373 if (items.nonEmpty) items(0) else null 374 375 def getDefaultComponent(root: java.awt.Container): java.awt.Component = 376 getFirstComponent(root) 377 378 def getLastComponent(root: java.awt.Container): java.awt.Component = 379 if (items.nonEmpty) items.last else null 380 } 381}