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}