equal
deleted
inserted
replaced
46 /* ignore wrt. keymap */ |
46 /* ignore wrt. keymap */ |
47 |
47 |
48 private def prop_ignore: String = property + ".ignore" |
48 private def prop_ignore: String = property + ".ignore" |
49 |
49 |
50 def ignored_keymaps(): List[String] = |
50 def ignored_keymaps(): List[String] = |
51 Library.space_explode(',', jEdit.getProperty(prop_ignore, "")) |
51 space_explode(',', jEdit.getProperty(prop_ignore, "")) |
52 |
52 |
53 def is_ignored(keymap_name: String): Boolean = |
53 def is_ignored(keymap_name: String): Boolean = |
54 ignored_keymaps().contains(keymap_name) |
54 ignored_keymaps().contains(keymap_name) |
55 |
55 |
56 def ignore(keymap_name: String): Unit = |
56 def ignore(keymap_name: String): Unit = |