diff --git a/static/web.js b/static/web.js index 10a42ff..fbc66a6 100644 --- a/static/web.js +++ b/static/web.js @@ -131,6 +131,9 @@ }; function rehighlight(pygmentized, language) { + if (language == "mir") { + pygmentized = formatMirScopes(pygmentized); + } var mappings = PYGMENTS_TO_ACE_MAPPINGS[language]; return pygmentized.replace(/([^<]*)<\/span>/g, function() { var classes = mappings[arguments[1]]; @@ -595,6 +598,10 @@ .replace(/<anon>:(\d+):(\d+)/mg, jumpToPoint); // new errors } + function formatMir(text) { + return text.replace(/<anon>:(\d+):(\d+):\s+(\d+):(\d+)/mg, jumpToRegion); + } + addEventListener("DOMContentLoaded", function() { evaluateButton = document.getElementById("evaluate"); asmButton = document.getElementById("asm");