equal
deleted
inserted
replaced
125 selected.value.contains(row) |
125 selected.value.contains(row) |
126 |
126 |
127 private def select(head: Int, tail: List[Int], b: Boolean): Unit = |
127 private def select(head: Int, tail: List[Int], b: Boolean): Unit = |
128 selected.change(set => if (b) set + head -- tail else set - head ++ tail) |
128 selected.change(set => if (b) set + head -- tail else set - head ++ tail) |
129 |
129 |
130 def apply(keymap_name: String, keymap: Keymap) |
130 def apply(keymap_name: String, keymap: Keymap): Unit = |
131 { |
131 { |
132 GUI_Thread.require {} |
132 GUI_Thread.require {} |
133 |
133 |
134 for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) { |
134 for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) { |
135 val b = is_selected(row) |
135 val b = is_selected(row) |
162 } |
162 } |
163 |
163 |
164 override def isCellEditable(row: Int, column: Int): Boolean = |
164 override def isCellEditable(row: Int, column: Int): Boolean = |
165 has_entry(row) && column == 0 |
165 has_entry(row) && column == 0 |
166 |
166 |
167 override def setValueAt(value: AnyRef, row: Int, column: Int) |
167 override def setValueAt(value: AnyRef, row: Int, column: Int): Unit = |
168 { |
168 { |
169 value match { |
169 value match { |
170 case obj: java.lang.Boolean if has_entry(row) && column == 0 => |
170 case obj: java.lang.Boolean if has_entry(row) && column == 0 => |
171 val b = obj.booleanValue |
171 val b = obj.booleanValue |
172 val entry = entries(row) |
172 val entry = entries(row) |
210 |
210 |
211 |
211 |
212 |
212 |
213 /** check with optional dialog **/ |
213 /** check with optional dialog **/ |
214 |
214 |
215 def check_dialog(view: View) |
215 def check_dialog(view: View): Unit = |
216 { |
216 { |
217 GUI_Thread.require {} |
217 GUI_Thread.require {} |
218 |
218 |
219 val keymap_manager = jEdit.getKeymapManager |
219 val keymap_manager = jEdit.getKeymapManager |
220 val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) |
220 val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) |