diff options
| author | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-12-07 12:55:17 +0000 |
|---|---|---|
| committer | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-12-07 12:55:17 +0000 |
| commit | 904e8029fea4436290fc79d5fabc782386cee19b (patch) | |
| tree | 6c5a6f0275acabd5ef72bb20798960c991dbaf37 /src/www/js | |
| parent | 81f843ac062541a7f3bec9fde23be560343b66b7 (diff) | |
Syntax editor: various small improvements...
- separate tree edit buttons from option buttons
- fix bug when wrapping on freshly imported ast
- add interface for import & export of ast
- cleaner internal implementation of Editor.add_refinement
- small style updates
Diffstat (limited to 'src/www/js')
| -rw-r--r-- | src/www/js/support.js | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/www/js/support.js b/src/www/js/support.js index 44c0e3895..9913aa5e3 100644 --- a/src/www/js/support.js +++ b/src/www/js/support.js @@ -248,6 +248,13 @@ function insertAfter(el,ref) { ref.parentNode.insertBefore(el,ref.nextSibling); } +function toggleHidden(el) { + if (el.classList.contains("hidden")) + el.classList.remove("hidden") + else + el.classList.add("hidden") +} + /* --- Debug ---------------------------------------------------------------- */ function debug(s) { |