Highlight spans in MIR comments

Author: mbrubeck

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 class="([^"]*)">([^<]*)<\/span>/g, function() {
             var classes = mappings[arguments[1]];
@@ -595,6 +598,10 @@
         .replace(/&lt;anon&gt;:(\d+):(\d+)/mg, jumpToPoint);  // new errors
     }
 
+    function formatMir(text) {
+        return text.replace(/&lt;anon&gt;:(\d+):(\d+):\s+(\d+):(\d+)/mg, jumpToRegion);
+    }
+
     addEventListener("DOMContentLoaded", function() {
         evaluateButton = document.getElementById("evaluate");
         asmButton = document.getElementById("asm");