diff options
| author |  Trevor Elliott <trevor@galois.com> | 2013-07-31 15:18:58 -0700 |
|---|---|---|
| committer | Trevor Elliott <trevor@galois.com> | 2013-07-31 15:18:58 -0700 |
| commit | fff553d47056306798f0742d9ae8b146ff27b6f9 (patch) | |
| tree | 40cb2d4e7c5ed26e9582eb9fc7a9284a5e15657a | |
| parent | 0201e0c683174f18e98084f5a06154bb16b532ec (diff) | |
Highlight problems from the new ui
| -rw-r--r-- | src/js/fiveui/injected/ui.js | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/js/fiveui/injected/ui.js b/src/js/fiveui/injected/ui.js index 03a1899..e02d83d 100644 --- a/src/js/fiveui/injected/ui.js +++ b/src/js/fiveui/injected/ui.js @@ -361,6 +361,8 @@ this.$el.one('click', _.bind(this.open, this)); this.$body.slideUp(100); + + core.maskProblem(this.problem); }, open:function() { @@ -369,6 +371,8 @@ this.$el.one('click', _.bind(this.close, this)); this.$body.slideDown(100); + + core.highlightProblem(this.problem); }, }); @@ -418,7 +422,7 @@ } else { // add the rule to the list of highlighted elements, and change its style // to look obvious. - var elt = core.query('.' + prob.hash); + var elt = fiveui.query('.' + prob.hash); var oldStyle = elt.attr('style'); core.maskRules(function() { @@ -441,7 +445,7 @@ obj.highlighted = obj.highlighted - 1; if(obj.highlighted == 0) { - var elt = core.query('.' + prob.hash); + var elt = fiveui.query('.' + prob.hash); // remove the fiveui style core.maskRules(function() { |