lean_highlight_rules.js 6.8 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156
  1. /* ***** BEGIN LICENSE BLOCK *****
  2. * Distributed under the BSD license:
  3. *
  4. * Copyright (c) 2010, Ajax.org B.V.
  5. * All rights reserved.
  6. *
  7. * Redistribution and use in source and binary forms, with or without
  8. * modification, are permitted provided that the following conditions are met:
  9. * * Redistributions of source code must retain the above copyright
  10. * notice, this list of conditions and the following disclaimer.
  11. * * Redistributions in binary form must reproduce the above copyright
  12. * notice, this list of conditions and the following disclaimer in the
  13. * documentation and/or other materials provided with the distribution.
  14. * * Neither the name of Ajax.org B.V. nor the
  15. * names of its contributors may be used to endorse or promote products
  16. * derived from this software without specific prior written permission.
  17. *
  18. * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
  19. * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
  20. * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
  21. * DISCLAIMED. IN NO EVENT SHALL AJAX.ORG B.V. BE LIABLE FOR ANY
  22. * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
  23. * (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  24. * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
  25. * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
  26. * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
  27. * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  28. *
  29. * ***** END LICENSE BLOCK ***** */
  30. define(function(require, exports, module) {
  31. "use strict";
  32. var oop = require("../lib/oop");
  33. var DocCommentHighlightRules = require("./doc_comment_highlight_rules").DocCommentHighlightRules;
  34. var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
  35. var leanHighlightRules = function() {
  36. var keywordControls = (
  37. [ "add_rewrite", "alias", "as", "assume", "attribute",
  38. "begin", "by", "calc", "calc_refl", "calc_subst", "calc_trans", "check",
  39. "classes", "coercions", "conjecture", "constants", "context",
  40. "corollary", "else", "end", "environment", "eval", "example",
  41. "exists", "exit", "export", "exposing", "extends", "fields", "find_decl",
  42. "forall", "from", "fun", "have", "help", "hiding", "if",
  43. "import", "in", "infix", "infixl", "infixr", "instances",
  44. "let", "local", "match", "namespace", "notation", "obtain", "obtains",
  45. "omit", "opaque", "open", "options", "parameter", "parameters", "postfix",
  46. "precedence", "prefix", "premise", "premises", "print", "private", "proof",
  47. "protected", "qed", "raw", "renaming", "section", "set_option",
  48. "show", "tactic_hint", "take", "then", "universe",
  49. "universes", "using", "variable", "variables", "with"].join("|")
  50. );
  51. var nameProviders = (
  52. ["inductive", "structure", "record", "theorem", "axiom",
  53. "axioms", "lemma", "hypothesis", "definition", "constant"].join("|")
  54. );
  55. var storageType = (
  56. ["Prop", "Type", "Type'", "Type₊", "Type₁", "Type₂", "Type₃"].join("|")
  57. );
  58. var storageModifiers = (
  59. "\\[(" +
  60. ["abbreviations", "all-transparent", "begin-end-hints", "class", "classes", "coercion",
  61. "coercions", "declarations", "decls", "instance", "irreducible",
  62. "multiple-instances", "notation", "notations", "parsing-only", "persistent",
  63. "reduce-hints", "reducible", "tactic-hints", "visible", "wf", "whnf"
  64. ].join("|") +
  65. ")\\]"
  66. );
  67. var keywordOperators = (
  68. [].join("|")
  69. );
  70. var keywordMapper = this.$keywords = this.createKeywordMapper({
  71. "keyword.control" : keywordControls,
  72. "storage.type" : storageType,
  73. "keyword.operator" : keywordOperators,
  74. "variable.language": "sorry",
  75. }, "identifier");
  76. var identifierRe = "[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f][A-Za-z0-9_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079\u207f-\u2089\u2090-\u209c\u2100-\u214f]*";
  77. var operatorRe = new RegExp(["#", "@", "->", "∼", "↔", "/", "==", "=", ":=", "<->",
  78. "/\\", "\\/", "∧", "∨", "≠", "<", ">", "≤", "≥", "¬",
  79. "<=", ">=", "⁻¹", "⬝", "▸", "\\+", "\\*", "-", "/",
  80. "λ", "→", "∃", "∀", ":="].join("|"));
  81. // regexp must not have capturing parentheses. Use (?:) instead.
  82. // regexps are ordered -> the first match is used
  83. this.$rules = {
  84. "start" : [
  85. {
  86. token : "comment", // single line comment "--"
  87. regex : "--.*$"
  88. },
  89. DocCommentHighlightRules.getStartRule("doc-start"),
  90. {
  91. token : "comment", // multi line comment "/-"
  92. regex : "\\/-",
  93. next : "comment"
  94. }, {
  95. stateName: "qqstring",
  96. token : "string.start", regex : '"', next : [
  97. {token : "string.end", regex : '"', next : "start"},
  98. {token : "constant.language.escape", regex : /\\[n"\\]/},
  99. {defaultToken: "string"}
  100. ]
  101. }, {
  102. token : "keyword.control", regex : nameProviders, next : [
  103. {token : "variable.language", regex : identifierRe, next : "start"} ]
  104. }, {
  105. token : "constant.numeric", // hex
  106. regex : "0[xX][0-9a-fA-F]+(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
  107. }, {
  108. token : "constant.numeric", // float
  109. regex : "[+-]?\\d+(?:(?:\\.\\d*)?(?:[eE][+-]?\\d+)?)?(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
  110. }, {
  111. token : "storage.modifier",
  112. regex : storageModifiers
  113. }, {
  114. token : keywordMapper,
  115. regex : identifierRe
  116. }, {
  117. token : "operator",
  118. regex : operatorRe
  119. }, {
  120. token : "punctuation.operator",
  121. regex : "\\?|\\:|\\,|\\;|\\."
  122. }, {
  123. token : "paren.lparen",
  124. regex : "[[({]"
  125. }, {
  126. token : "paren.rparen",
  127. regex : "[\\])}]"
  128. }, {
  129. token : "text",
  130. regex : "\\s+"
  131. }
  132. ],
  133. "comment" : [ {token: "comment", regex: "-/", next: "start"},
  134. {defaultToken: "comment"} ]
  135. };
  136. this.embedRules(DocCommentHighlightRules, "doc-",
  137. [ DocCommentHighlightRules.getEndRule("start") ]);
  138. this.normalizeRules();
  139. };
  140. oop.inherits(leanHighlightRules, TextHighlightRules);
  141. exports.leanHighlightRules = leanHighlightRules;
  142. });