aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Trevor Elliott <trevor@galois.com>2013-06-17 17:17:09 -0700
committerGravatar Trevor Elliott <trevor@galois.com>2013-06-17 17:24:54 -0700
commit8316c65b174e881433721382e0214cec2412ae6b (patch)
treee3c1c00b1ebbb1578218104ebf752028d23927a3 /src
parent7a4a58de847fd2ebe50c30e4874eea4c057c065f (diff)
Fix a funny bug that caused a closed port to be used
Diffstat (limited to 'src')
-rw-r--r--src/js/fiveui/injected/compute.js10
-rw-r--r--src/js/fiveui/injected/ui.js40
-rw-r--r--src/js/fiveui/js/background.js9
3 files changed, 44 insertions, 15 deletions
diff --git a/src/js/fiveui/injected/compute.js b/src/js/fiveui/injected/compute.js
index 8fc7a84..7ba4af4 100644
--- a/src/js/fiveui/injected/compute.js
+++ b/src/js/fiveui/injected/compute.js
@@ -90,15 +90,6 @@
core.port.emit('ReportProblem', prob);
};
- core.resetStats = function() {
- core.reportStats(
- { start: 0
- , end: 0
- , numRules: 0
- , numElts: 0
- });
- };
-
core.reportStats = function(stats) {
core.port.emit('ReportStats', stats);
};
@@ -356,6 +347,5 @@
};
registerBackendListeners(core.port);
- core.resetStats();
})();
diff --git a/src/js/fiveui/injected/ui.js b/src/js/fiveui/injected/ui.js
index a61b122..d742720 100644
--- a/src/js/fiveui/injected/ui.js
+++ b/src/js/fiveui/injected/ui.js
@@ -85,15 +85,42 @@
});
};
+ core.renderStatsTemplate = _.template(
+ [ '<table class="fiveui-table">'
+ , ' <tr>'
+ , ' <td class="fiveui-table-text">rules checked:</td>'
+ , ' <td class="fiveui-table-number"><%= numRules %></td>'
+ , ' </tr>'
+ , ' <tr>'
+ , ' <td class="fiveui-table-text">elements checked:</td>'
+ , ' <td class="fiveui-table-number"><%= numElts %></td>'
+ , ' </tr>'
+ , ' <tr>'
+ , ' <td class="fiveui-table-text">elapsed time (ms):</td>'
+ , ' <td class="fiveui-table-number"><%= time %></td>'
+ , ' </tr>'
+ , '</table>'
+ ].join(''));
+
core.renderStats = function (stats) {
+
+ // give stats some sane defaults.
+ stats = stats || {};
+ _.defaults(stats, {
+ numRules: 0,
+ numElts: 0,
+ start: 0,
+ end: 0,
+ });
+
core.maskRules(function () {
+
var statsDiv, statsDetail;
statsDiv = $('#fiveui-stats');
statsDiv.children().remove();
- statsDetail = $('<table class="fiveui-table"><tr><td class="fiveui-table-text">rules checked:</td><td class="fiveui-table-number">' + stats.numRules + '</td></tr>' +
- '<tr><td class="fiveui-table-text">elements checked:</td><td class="fiveui-table-number">' + stats.numElts + '</td></tr>' +
- '<tr><td class="fiveui-table-text">elapsed time (ms):</td><td class="fiveui-table-number">' + (stats.end - stats.start) + '</td></tr></table>');
- statsDiv.append(statsDetail);
+
+ stats.time = stats.end - stats.start;
+ statsDiv.html(core.renderStatsTemplate(stats));
});
};
@@ -211,11 +238,13 @@
$('#clearButton').click(function() {
$('#problemList').children().remove();
port.emit('ClearProblems');
- core.renderStats(fiveui.stats.zero);
+
+ core.renderStats();
$('prExpand-down').click();
// Just in case the click event on prExpand-down missde anything:
core.maskProblem(fiveui.query('.uic-problem'), undefined);
+ core.renderStats();
});
///////////////////////////////////////////
@@ -239,6 +268,7 @@
$(state.problems).each(function(ix,prob) {
core.renderProblem(prob);
});
+
core.renderStats(state.stats);
});
};
diff --git a/src/js/fiveui/js/background.js b/src/js/fiveui/js/background.js
index c52aca8..dfe0649 100644
--- a/src/js/fiveui/js/background.js
+++ b/src/js/fiveui/js/background.js
@@ -50,6 +50,12 @@ fiveui.Background = function(settings, updateWidget, loadScripts, dataLoader) {
this.dataLoader = dataLoader;
};
+/**
+ * NOTE: As compute nodes get injected first, there's a chance that if send
+ * ReportProblem or ReportStats too early, the uiPort element of the tabState
+ * might not be setup yet. This will cause some strange problems, and we should
+ * consider reversing the order that the injection happens in.
+ */
fiveui.Background.prototype._registerComputeListeners = function(port, tabState){
var bg = this;
port.on('ReportProblem', function(request) {
@@ -134,6 +140,9 @@ fiveui.Background.prototype.pageLoad = function(tabId, url, data) {
this.updateWidget(null);
} else {
var tabState = this.state.acquireTabState(tabId);
+
+ // clear out old ports
+ tabState.uiPort = null;
tabState.computePorts = [];
this.updateWidget(tabState);