matita/matita/nlibrary/topology/sh_main.js

   1 /*\r
   2 SHJS - Syntax Highlighting in JavaScript\r
   3 Copyright (C) 2007, 2008 gnombat@users.sourceforge.net\r
   4 License: http://shjs.sourceforge.net/doc/gplv3.html\r
   5 */\r
   6 \r
   7 if (! this.sh_languages) {\r
   8   this.sh_languages = {};\r
   9 }\r
  10 var sh_requests = {};\r
  11 \r
  12 function sh_isEmailAddress(url) {\r
  13   if (/^mailto:/.test(url)) {\r
  14     return false;\r
  15   }\r
  16   return url.indexOf('@') !== -1;\r
  17 }\r
  18 \r
  19 function sh_setHref(tags, numTags, inputString) {\r
  20   var url = inputString.substring(tags[numTags - 2].pos, tags[numTags - 1].pos);\r
  21   if (url.length >= 2 && url.charAt(0) === '<' && url.charAt(url.length - 1) === '>') {\r
  22     url = url.substr(1, url.length - 2);\r
  23   }\r
  24   if (sh_isEmailAddress(url)) {\r
  25     url = 'mailto:' + url;\r
  26   }\r
  27   tags[numTags - 2].node.href = url;\r
  28 }\r
  29 \r
  30 /*\r
  31 Konqueror has a bug where the regular expression /$/g will not match at the end\r
  32 of a line more than once:\r
  33 \r
  34   var regex = /$/g;\r
  35   var match;\r
  36 \r
  37   var line = '1234567890';\r
  38   regex.lastIndex = 10;\r
  39   match = regex.exec(line);\r
  40 \r
  41   var line2 = 'abcde';\r
  42   regex.lastIndex = 5;\r
  43   match = regex.exec(line2);  // fails\r
  44 */\r
  45 function sh_konquerorExec(s) {\r
  46   var result = [''];\r
  47   result.index = s.length;\r
  48   result.input = s;\r
  49   return result;\r
  50 }\r
  51 \r
  52 /**\r
  53 Highlights all elements containing source code in a text string.  The return\r
  54 value is an array of objects, each representing an HTML start or end tag.  Each\r
  55 object has a property named pos, which is an integer representing the text\r
  56 offset of the tag. Every start tag also has a property named node, which is the\r
  57 DOM element started by the tag. End tags do not have this property.\r
  58 @param  inputString  a text string\r
  59 @param  language  a language definition object\r
  60 @return  an array of tag objects\r
  61 */\r
  62 function sh_highlightString(inputString, language) {\r
  63   if (/Konqueror/.test(navigator.userAgent)) {\r
  64     if (! language.konquered) {\r
  65       for (var s = 0; s < language.length; s++) {\r
  66         for (var p = 0; p < language[s].length; p++) {\r
  67           var r = language[s][p][0];\r
  68           if (r.source === '$') {\r
  69             r.exec = sh_konquerorExec;\r
  70           }\r
  71         }\r
  72       }\r
  73       language.konquered = true;\r
  74     }\r
  75   }\r
  76 \r
  77   var a = document.createElement('a');\r
  78   var span = document.createElement('span');\r
  79 \r
  80   // the result\r
  81   var tags = [];\r
  82   var numTags = 0;\r
  83 \r
  84   // each element is a pattern object from language\r
  85   var patternStack = [];\r
  86 \r
  87   // the current position within inputString\r
  88   var pos = 0;\r
  89 \r
  90   // the name of the current style, or null if there is no current style\r
  91   var currentStyle = null;\r
  92 \r
  93   var output = function(s, style) {\r
  94     var length = s.length;\r
  95     // this is more than just an optimization - we don't want to output empty <span></span> elements\r
  96     if (length === 0) {\r
  97       return;\r
  98     }\r
  99     if (! style) {\r
 100       var stackLength = patternStack.length;\r
 101       if (stackLength !== 0) {\r
 102         var pattern = patternStack[stackLength - 1];\r
 103         // check whether this is a state or an environment\r
 104         if (! pattern[3]) {\r
 105           // it's not a state - it's an environment; use the style for this environment\r
 106           style = pattern[1];\r
 107         }\r
 108       }\r
 109     }\r
 110     if (currentStyle !== style) {\r
 111       if (currentStyle) {\r
 112         tags[numTags++] = {pos: pos};\r
 113         if (currentStyle === 'sh_url') {\r
 114           sh_setHref(tags, numTags, inputString);\r
 115         }\r
 116       }\r
 117       if (style) {\r
 118         var clone;\r
 119         if (style === 'sh_url') {\r
 120           clone = a.cloneNode(false);\r
 121         }\r
 122         else {\r
 123           clone = span.cloneNode(false);\r
 124         }\r
 125         clone.className = style;\r
 126         tags[numTags++] = {node: clone, pos: pos};\r
 127       }\r
 128     }\r
 129     pos += length;\r
 130     currentStyle = style;\r
 131   };\r
 132 \r
 133   var endOfLinePattern = /\r\n|\r|\n/g;\r
 134   endOfLinePattern.lastIndex = 0;\r
 135   var inputStringLength = inputString.length;\r
 136   while (pos < inputStringLength) {\r
 137     var start = pos;\r
 138     var end;\r
 139     var startOfNextLine;\r
 140     var endOfLineMatch = endOfLinePattern.exec(inputString);\r
 141     if (endOfLineMatch === null) {\r
 142       end = inputStringLength;\r
 143       startOfNextLine = inputStringLength;\r
 144     }\r
 145     else {\r
 146       end = endOfLineMatch.index;\r
 147       startOfNextLine = endOfLinePattern.lastIndex;\r
 148     }\r
 149 \r
 150     var line = inputString.substring(start, end);\r
 151 \r
 152     var matchCache = [];\r
 153     for (;;) {\r
 154       var posWithinLine = pos - start;\r
 155 \r
 156       var stateIndex;\r
 157       var stackLength = patternStack.length;\r
 158       if (stackLength === 0) {\r
 159         stateIndex = 0;\r
 160       }\r
 161       else {\r
 162         // get the next state\r
 163         stateIndex = patternStack[stackLength - 1][2];\r
 164       }\r
 165 \r
 166       var state = language[stateIndex];\r
 167       var numPatterns = state.length;\r
 168       var mc = matchCache[stateIndex];\r
 169       if (! mc) {\r
 170         mc = matchCache[stateIndex] = [];\r
 171       }\r
 172       var bestMatch = null;\r
 173       var bestPatternIndex = -1;\r
 174       for (var i = 0; i < numPatterns; i++) {\r
 175         var match;\r
 176         if (i < mc.length && (mc[i] === null || posWithinLine <= mc[i].index)) {\r
 177           match = mc[i];\r
 178         }\r
 179         else {\r
 180           var regex = state[i][0];\r
 181           regex.lastIndex = posWithinLine;\r
 182           match = regex.exec(line);\r
 183           mc[i] = match;\r
 184         }\r
 185         if (match !== null && (bestMatch === null || match.index < bestMatch.index)) {\r
 186           bestMatch = match;\r
 187           bestPatternIndex = i;\r
 188           if (match.index === posWithinLine) {\r
 189             break;\r
 190           }\r
 191         }\r
 192       }\r
 193 \r
 194       if (bestMatch === null) {\r
 195         output(line.substring(posWithinLine), null);\r
 196         break;\r
 197       }\r
 198       else {\r
 199         // got a match\r
 200         if (bestMatch.index > posWithinLine) {\r
 201           output(line.substring(posWithinLine, bestMatch.index), null);\r
 202         }\r
 203 \r
 204         var pattern = state[bestPatternIndex];\r
 205 \r
 206         var newStyle = pattern[1];\r
 207         var matchedString;\r
 208         if (newStyle instanceof Array) {\r
 209           for (var subexpression = 0; subexpression < newStyle.length; subexpression++) {\r
 210             matchedString = bestMatch[subexpression + 1];\r
 211             output(matchedString, newStyle[subexpression]);\r
 212           }\r
 213         }\r
 214         else {\r
 215           matchedString = bestMatch[0];\r
 216           output(matchedString, newStyle);\r
 217         }\r
 218 \r
 219         switch (pattern[2]) {\r
 220         case -1:\r
 221           // do nothing\r
 222           break;\r
 223         case -2:\r
 224           // exit\r
 225           patternStack.pop();\r
 226           break;\r
 227         case -3:\r
 228           // exitall\r
 229           patternStack.length = 0;\r
 230           break;\r
 231         default:\r
 232           // this was the start of a delimited pattern or a state/environment\r
 233           patternStack.push(pattern);\r
 234           break;\r
 235         }\r
 236       }\r
 237     }\r
 238 \r
 239     // end of the line\r
 240     if (currentStyle) {\r
 241       tags[numTags++] = {pos: pos};\r
 242       if (currentStyle === 'sh_url') {\r
 243         sh_setHref(tags, numTags, inputString);\r
 244       }\r
 245       currentStyle = null;\r
 246     }\r
 247     pos = startOfNextLine;\r
 248   }\r
 249 \r
 250   return tags;\r
 251 }\r
 252 \r
 253 ////////////////////////////////////////////////////////////////////////////////\r
 254 // DOM-dependent functions\r
 255 \r
 256 function sh_getClasses(element) {\r
 257   var result = [];\r
 258   var htmlClass = element.className;\r
 259   if (htmlClass && htmlClass.length > 0) {\r
 260     var htmlClasses = htmlClass.split(' ');\r
 261     for (var i = 0; i < htmlClasses.length; i++) {\r
 262       if (htmlClasses[i].length > 0) {\r
 263         result.push(htmlClasses[i]);\r
 264       }\r
 265     }\r
 266   }\r
 267   return result;\r
 268 }\r
 269 \r
 270 function sh_addClass(element, name) {\r
 271   var htmlClasses = sh_getClasses(element);\r
 272   for (var i = 0; i < htmlClasses.length; i++) {\r
 273     if (name.toLowerCase() === htmlClasses[i].toLowerCase()) {\r
 274       return;\r
 275     }\r
 276   }\r
 277   htmlClasses.push(name);\r
 278   element.className = htmlClasses.join(' ');\r
 279 }\r
 280 \r
 281 /**\r
 282 Extracts the tags from an HTML DOM NodeList.\r
 283 @param  nodeList  a DOM NodeList\r
 284 @param  result  an object with text, tags and pos properties\r
 285 */\r
 286 function sh_extractTagsFromNodeList(nodeList, result) {\r
 287   var length = nodeList.length;\r
 288   for (var i = 0; i < length; i++) {\r
 289     var node = nodeList.item(i);\r
 290     switch (node.nodeType) {\r
 291     case 1:\r
 292       if (node.nodeName.toLowerCase() === 'br') {\r
 293         var terminator;\r
 294         if (/MSIE/.test(navigator.userAgent)) {\r
 295           terminator = '\r';\r
 296         }\r
 297         else {\r
 298           terminator = '\n';\r
 299         }\r
 300         result.text.push(terminator);\r
 301         result.pos++;\r
 302       }\r
 303       else {\r
 304         result.tags.push({node: node.cloneNode(false), pos: result.pos});\r
 305         sh_extractTagsFromNodeList(node.childNodes, result);\r
 306         result.tags.push({pos: result.pos});\r
 307       }\r
 308       break;\r
 309     case 3:\r
 310     case 4:\r
 311       result.text.push(node.data);\r
 312       result.pos += node.length;\r
 313       break;\r
 314     }\r
 315   }\r
 316 }\r
 317 \r
 318 /**\r
 319 Extracts the tags from the text of an HTML element. The extracted tags will be\r
 320 returned as an array of tag objects. See sh_highlightString for the format of\r
 321 the tag objects.\r
 322 @param  element  a DOM element\r
 323 @param  tags  an empty array; the extracted tag objects will be returned in it\r
 324 @return  the text of the element\r
 325 @see  sh_highlightString\r
 326 */\r
 327 function sh_extractTags(element, tags) {\r
 328   var result = {};\r
 329   result.text = [];\r
 330   result.tags = tags;\r
 331   result.pos = 0;\r
 332   sh_extractTagsFromNodeList(element.childNodes, result);\r
 333   return result.text.join('');\r
 334 }\r
 335 \r
 336 /**\r
 337 Merges the original tags from an element with the tags produced by highlighting.\r
 338 @param  originalTags  an array containing the original tags\r
 339 @param  highlightTags  an array containing the highlighting tags - these must not overlap\r
 340 @result  an array containing the merged tags\r
 341 */\r
 342 function sh_mergeTags(originalTags, highlightTags) {\r
 343   var numOriginalTags = originalTags.length;\r
 344   if (numOriginalTags === 0) {\r
 345     return highlightTags;\r
 346   }\r
 347 \r
 348   var numHighlightTags = highlightTags.length;\r
 349   if (numHighlightTags === 0) {\r
 350     return originalTags;\r
 351   }\r
 352 \r
 353   var result = [];\r
 354   var originalIndex = 0;\r
 355   var highlightIndex = 0;\r
 356 \r
 357   while (originalIndex < numOriginalTags && highlightIndex < numHighlightTags) {\r
 358     var originalTag = originalTags[originalIndex];\r
 359     var highlightTag = highlightTags[highlightIndex];\r
 360 \r
 361     if (originalTag.pos <= highlightTag.pos) {\r
 362       result.push(originalTag);\r
 363       originalIndex++;\r
 364     }\r
 365     else {\r
 366       result.push(highlightTag);\r
 367       if (highlightTags[highlightIndex + 1].pos <= originalTag.pos) {\r
 368         highlightIndex++;\r
 369         result.push(highlightTags[highlightIndex]);\r
 370         highlightIndex++;\r
 371       }\r
 372       else {\r
 373         // new end tag\r
 374         result.push({pos: originalTag.pos});\r
 375 \r
 376         // new start tag\r
 377         highlightTags[highlightIndex] = {node: highlightTag.node.cloneNode(false), pos: originalTag.pos};\r
 378       }\r
 379     }\r
 380   }\r
 381 \r
 382   while (originalIndex < numOriginalTags) {\r
 383     result.push(originalTags[originalIndex]);\r
 384     originalIndex++;\r
 385   }\r
 386 \r
 387   while (highlightIndex < numHighlightTags) {\r
 388     result.push(highlightTags[highlightIndex]);\r
 389     highlightIndex++;\r
 390   }\r
 391 \r
 392   return result;\r
 393 }\r
 394 \r
 395 /**\r
 396 Inserts tags into text.\r
 397 @param  tags  an array of tag objects\r
 398 @param  text  a string representing the text\r
 399 @return  a DOM DocumentFragment representing the resulting HTML\r
 400 */\r
 401 function sh_insertTags(tags, text) {\r
 402   var doc = document;\r
 403 \r
 404   var result = document.createDocumentFragment();\r
 405   var tagIndex = 0;\r
 406   var numTags = tags.length;\r
 407   var textPos = 0;\r
 408   var textLength = text.length;\r
 409   var currentNode = result;\r
 410 \r
 411   // output one tag or text node every iteration\r
 412   while (textPos < textLength || tagIndex < numTags) {\r
 413     var tag;\r
 414     var tagPos;\r
 415     if (tagIndex < numTags) {\r
 416       tag = tags[tagIndex];\r
 417       tagPos = tag.pos;\r
 418     }\r
 419     else {\r
 420       tagPos = textLength;\r
 421     }\r
 422 \r
 423     if (tagPos <= textPos) {\r
 424       // output the tag\r
 425       if (tag.node) {\r
 426         // start tag\r
 427         var newNode = tag.node;\r
 428         currentNode.appendChild(newNode);\r
 429         currentNode = newNode;\r
 430       }\r
 431       else {\r
 432         // end tag\r
 433         currentNode = currentNode.parentNode;\r
 434       }\r
 435       tagIndex++;\r
 436     }\r
 437     else {\r
 438       // output text\r
 439       currentNode.appendChild(doc.createTextNode(text.substring(textPos, tagPos)));\r
 440       textPos = tagPos;\r
 441     }\r
 442   }\r
 443 \r
 444   return result;\r
 445 }\r
 446 \r
 447 /**\r
 448 Highlights an element containing source code.  Upon completion of this function,\r
 449 the element will have been placed in the "sh_sourceCode" class.\r
 450 @param  element  a DOM <pre> element containing the source code to be highlighted\r
 451 @param  language  a language definition object\r
 452 */\r
 453 function sh_highlightElement(element, language) {\r
 454   sh_addClass(element, 'sh_sourceCode');\r
 455   var originalTags = [];\r
 456   var inputString = sh_extractTags(element, originalTags);\r
 457   var highlightTags = sh_highlightString(inputString, language);\r
 458   var tags = sh_mergeTags(originalTags, highlightTags);\r
 459   var documentFragment = sh_insertTags(tags, inputString);\r
 460   while (element.hasChildNodes()) {\r
 461     element.removeChild(element.firstChild);\r
 462   }\r
 463   element.appendChild(documentFragment);\r
 464 }\r
 465 \r
 466 function sh_getXMLHttpRequest() {\r
 467   if (window.ActiveXObject) {\r
 468     return new ActiveXObject('Msxml2.XMLHTTP');\r
 469   }\r
 470   else if (window.XMLHttpRequest) {\r
 471     return new XMLHttpRequest();\r
 472   }\r
 473   throw 'No XMLHttpRequest implementation available';\r
 474 }\r
 475 \r
 476 function sh_load(language, element, prefix, suffix) {\r
 477   if (language in sh_requests) {\r
 478     sh_requests[language].push(element);\r
 479     return;\r
 480   }\r
 481   sh_requests[language] = [element];\r
 482   var request = sh_getXMLHttpRequest();\r
 483   var url = prefix + 'sh_' + language + suffix;\r
 484   request.open('GET', url, true);\r
 485   request.onreadystatechange = function () {\r
 486     if (request.readyState === 4) {\r
 487       try {\r
 488         if (! request.status || request.status === 200) {\r
 489           eval(request.responseText);\r
 490           var elements = sh_requests[language];\r
 491           for (var i = 0; i < elements.length; i++) {\r
 492             sh_highlightElement(elements[i], sh_languages[language]);\r
 493           }\r
 494         }\r
 495         else {\r
 496           throw 'HTTP error: status ' + request.status;\r
 497         }\r
 498       }\r
 499       finally {\r
 500         request = null;\r
 501       }\r
 502     }\r
 503   };\r
 504   request.send(null);\r
 505 }\r
 506 \r
 507 /**\r
 508 Highlights all elements containing source code on the current page. Elements\r
 509 containing source code must be "pre" elements with a "class" attribute of\r
 510 "sh_LANGUAGE", where LANGUAGE is a valid language identifier; e.g., "sh_java"\r
 511 identifies the element as containing "java" language source code.\r
 512 */\r
 513 function sh_highlightDocument(prefix, suffix) {\r
 514   var nodeList = document.getElementsByTagName('pre');\r
 515   for (var i = 0; i < nodeList.length; i++) {\r
 516     var element = nodeList.item(i);\r
 517     var htmlClasses = sh_getClasses(element);\r
 518     for (var j = 0; j < htmlClasses.length; j++) {\r
 519       var htmlClass = htmlClasses[j].toLowerCase();\r
 520       if (htmlClass === 'sh_sourcecode') {\r
 521         continue;\r
 522       }\r
 523       if (htmlClass.substr(0, 3) === 'sh_') {\r
 524         var language = htmlClass.substring(3);\r
 525         if (language in sh_languages) {\r
 526           sh_highlightElement(element, sh_languages[language]);\r
 527         }\r
 528         else if (typeof(prefix) === 'string' && typeof(suffix) === 'string') {\r
 529           sh_load(language, element, prefix, suffix);\r
 530         }\r
 531         else {\r
 532           throw 'Found <pre> element with class="' + htmlClass + '", but no such language exists';\r
 533         }\r
 534         break;\r
 535       }\r
 536     }\r
 537   }\r
 538 }\r