src/Tools/VSCode/src/grammar.scala
author wenzelm
Mon Jan 02 10:22:59 2017 +0100 (2017-01-02)
changeset 64745 0f002c15f3ab
parent 64744 ba0d4829d5f1
child 64746 34db87033abe
permissions -rw-r--r--
more syntax;
tuned;
     1 /*  Title:      Tools/VSCode/src/grammar.scala
     2     Author:     Makarius
     3 
     4 Generate static TextMate grammar for VSCode editor.
     5 */
     6 
     7 package isabelle.vscode
     8 
     9 
    10 import isabelle._
    11 
    12 import java.util.UUID
    13 
    14 
    15 object Grammar
    16 {
    17   /* generate grammar */
    18 
    19   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    20 
    21   private def default_output(logic: String = ""): String =
    22     if (logic == "" || logic == default_logic) "isabelle-grammar.json"
    23     else "isabelle-" + logic + "-grammar.json"
    24 
    25   def generate(keywords: Keyword.Keywords): JSON.S =
    26   {
    27     val (minor_keywords, operators) =
    28       keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier(_))
    29 
    30     def major_keywords(pred: String => Boolean): List[String] =
    31       (for {
    32         k <- keywords.major.iterator
    33         kind <- keywords.kinds.get(k)
    34         if pred(kind)
    35       } yield k).toList
    36 
    37     val keywords1 =
    38       major_keywords(k => k != Keyword.THY_END && k != Keyword.PRF_ASM && k != Keyword.PRF_ASM_GOAL)
    39     val keywords2 = minor_keywords ::: major_keywords(Set(Keyword.THY_END))
    40     val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL))
    41 
    42 
    43     def quote_name(a: String): String =
    44       if (Symbol.is_ascii_identifier(a)) a else "\\Q" + a + "\\E"
    45 
    46     def grouped_names(as: List[String]): String =
    47       JSON.Format("\\b(" + as.sorted.map(quote_name(_)).mkString("|") + ")\\b")
    48 
    49     """{
    50   "name": "Isabelle",
    51   "scopeName": "source.isabelle",
    52   "fileTypes": ["thy"],
    53   "uuid": """ + JSON.Format(UUID.randomUUID().toString) + """,
    54   "repository": {
    55     "comment": {
    56       "patterns": [
    57         {
    58           "name": "comment.block.isabelle",
    59           "begin": "\\(\\*",
    60           "beginCaptures": {
    61             "0": { "name": "punctuation.definition.comment.begin.isabelle" }
    62           },
    63           "patterns": [{ "include": "#comment" }],
    64           "end": "\\*\\)",
    65           "endCaptures": {
    66             "0": { "name": "punctuation.definition.comment.end.isabelle" }
    67           }
    68         }
    69       ]
    70     },
    71     "cartouche": {
    72       "patterns": [
    73         {
    74           "name": "string.quoted.other.multiline.isabelle",
    75           "begin": "(?:\\\\<open>|‹)",
    76           "beginCaptures": {
    77             "0": { "name": "punctuation.definition.string.begin.isabelle" }
    78           },
    79           "patterns": [{ "include": "#cartouche" }],
    80           "end": "(?:\\\\<close>|›)",
    81           "endCaptures": {
    82             "0": { "name": "punctuation.definition.string.end.isabelle" }
    83           }
    84         }
    85       ]
    86     }
    87   },
    88   "patterns": [
    89     {
    90       "include": "#comment"
    91     },
    92     {
    93       "include": "#cartouche"
    94     },
    95     {
    96       "name": "keyword.control.isabelle",
    97       "match": """ + grouped_names(keywords1) + """
    98     },
    99     {
   100       "name": "keyword.other.isabelle",
   101       "match": """ + grouped_names(keywords2) + """
   102     },
   103     {
   104       "name": "keyword.operator.isabelle",
   105       "match": """ + grouped_names(operators) + """
   106     },
   107     {
   108       "name": "constant.language.isabelle",
   109       "match": """ + grouped_names(keywords3) + """
   110     },
   111     {
   112       "match": "\\b\\d*\\.?\\d+\\b",
   113       "name": "constant.numeric.isabelle"
   114     },
   115     {
   116       "name": "string.quoted.double.isabelle",
   117       "begin": "\"",
   118       "beginCaptures": {
   119         "0": { "name": "punctuation.definition.string.begin.isabelle" }
   120       },
   121       "patterns": [
   122         {
   123           "match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """,
   124           "name": "constant.character.escape.isabelle"
   125         }
   126       ],
   127       "end": "\"",
   128       "endCaptures": {
   129         "0": { "name": "punctuation.definition.string.end.isabelle" }
   130       }
   131     },
   132     {
   133       "name": "string.quoted.backtick.isabelle",
   134       "begin": "`",
   135       "beginCaptures": {
   136         "0": { "name": "punctuation.definition.string.begin.isabelle" }
   137       },
   138       "patterns": [
   139         {
   140           "match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """,
   141           "name": "constant.character.escape.isabelle"
   142         }
   143       ],
   144       "end": "`",
   145       "endCaptures": {
   146         "0": { "name": "punctuation.definition.string.end.isabelle" }
   147       }
   148     }
   149   ]
   150 }
   151 """
   152   }
   153 
   154 
   155   /* Isabelle tool wrapper */
   156 
   157   val isabelle_tool = Isabelle_Tool("vscode_grammar",
   158     "generate static TextMate grammar for VSCode editor", args =>
   159   {
   160     var dirs: List[Path] = Nil
   161     var logic = default_logic
   162     var output: Option[Path] = None
   163 
   164     val getopts = Getopts("""
   165 Usage: isabelle vscode_grammar [OPTIONS]
   166 
   167   Options are:
   168     -d DIR       include session directory
   169     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
   170     -o FILE      output file name (default """ + default_output() + """)
   171 
   172   Generate static TextMate grammar for VSCode editor.
   173 """,
   174       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   175       "l:" -> (arg => logic = arg),
   176       "o:" -> (arg => output = Some(Path.explode(arg))))
   177 
   178     val more_args = getopts(args)
   179     if (more_args.nonEmpty) getopts.usage()
   180 
   181     val keywords = Build.outer_syntax(Options.init(), dirs, logic).keywords
   182     val output_path = output getOrElse Path.explode(default_output(logic))
   183 
   184     Output.writeln(output_path.implode)
   185     File.write_backup(output_path, generate(keywords))
   186   })
   187 }