diff options
| author | Camil Staps | 2015-05-08 12:54:40 +0300 |
|---|---|---|
| committer | Camil Staps | 2015-05-08 12:54:40 +0300 |
| commit | b7cefbb8906a6edad4fd5445c50c41adba582b87 (patch) | |
| tree | de56ce91760eba2134428a06f9c64bc77d4f7055 | |
| parent | Initial commit (diff) | |
This seems to work
| -rw-r--r-- | coqCounter.js | 30 | ||||
| -rw-r--r-- | index.html | 18 |
2 files changed, 48 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 diff --git a/index.html b/index.html new file mode 100644 index 0000000..549b2cb --- /dev/null +++ b/index.html @@ -0,0 +1,18 @@ +<!DOCTYPE html> +<html> + <head> + <title>Coq commands counter</title> + </head> + <body> + <textarea id="input" cols="60" rows="20"></textarea><br/> + <textarea id="output" cols="60" rows="2"></textarea> + + <script type="text/javascript" src="//code.jquery.com/jquery-1.11.3.min.js"></script> + <script type="text/javascript" src="coqCounter.js"></script> + <script type="text/javascript"> + $(function(){ + $('#input').coqCounter('#output'); + }); + </script> + </body> +</html>
\ No newline at end of file |