equal
deleted
inserted
replaced
110 option_type, JOptionPane.QUESTION_MESSAGE) |
110 option_type, JOptionPane.QUESTION_MESSAGE) |
111 } |
111 } |
112 |
112 |
113 |
113 |
114 /* basic GUI components */ |
114 /* basic GUI components */ |
|
115 |
|
116 class Button(label: String) extends scala.swing.Button(label) { |
|
117 def clicked(): Unit = {} |
|
118 |
|
119 reactions += { case ButtonClicked(_) => clicked() } |
|
120 } |
115 |
121 |
116 class Bool(label: String, init: Boolean = false) extends CheckBox(label) { |
122 class Bool(label: String, init: Boolean = false) extends CheckBox(label) { |
117 def clicked(state: Boolean): Unit = {} |
123 def clicked(state: Boolean): Unit = {} |
118 def clicked(): Unit = {} |
124 def clicked(): Unit = {} |
119 |
125 |