This seems to work

1 files changed, 30 insertions, 0 deletions

diff --git a/coqCounter.js b/coqCounter.js
new file mode 100644
index 0000000..72f7ad7
--- /dev/null
+++ b/coqCounter.js
@@ -0,0 +1,30 @@
+$.fn.coqCounter = function(output) {
+    $(this).change(function(){
+        var regex = /[\n^]([a-zA-Z_'0-9]+)/g;
+        var value = $(this).val();
+        var matches = [], i = 0;
+
+        do {
+            match = regex.exec(value);
+            if (match != null) {
+                matches[i++] = match[1];
+            }
+        } while (match != null);
+
+        matches.sort();
+
+        var counts = {};
+        matches.forEach(function(x) { counts[x] = (counts[x] || 0)+1; });
+
+        var counts_output = [], i = 0;
+        for (cmd in counts) {
+            counts_output[i++] = counts[cmd] + "x " + cmd;
+        }
+
+        console.log(counts_output);
+
+        $(output).val(counts_output.join(", "));
+    });
+
+    return this;
+};
\ No newline at end of file