src/Tools/VSCode/src/grammar.scala
author wenzelm
Mon Jan 02 09:41:25 2017 +0100 (2017-01-02)
changeset 64744 ba0d4829d5f1
parent 64742 5f946e8887c5
child 64745 0f002c15f3ab
permissions -rw-r--r--
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     "comments": {
    56       "patterns": [
    57         {
    58           "name": "comment.block.isabelle",
    59           "begin": "\\(\\*",
    60           "beginCaptures": {
    61             "0": { "name": "punctuation.definition.comment.begin.isabelle" }
    62           },
    63           "patterns": [{ "include": "#comments" }],
    64           "end": "\\*\\)",
    65           "endCaptures": {
    66             "0": { "name": "punctuation.definition.comment.end.isabelle" }
    67           }
    68         }
    69       ]
    70     }
    71   },
    72   "patterns": [
    73     {
    74       "include": "#comments"
    75     },
    76     {
    77       "name": "keyword.control.isabelle",
    78       "match": """ + grouped_names(keywords1) + """
    79     },
    80     {
    81       "name": "keyword.other.isabelle",
    82       "match": """ + grouped_names(keywords2) + """
    83     },
    84     {
    85       "name": "keyword.operator.isabelle",
    86       "match": """ + grouped_names(operators) + """
    87     },
    88     {
    89       "name": "constant.language.isabelle",
    90       "match": """ + grouped_names(keywords3) + """
    91     },
    92     {
    93       "match": "\\b\\d*\\.?\\d+\\b",
    94       "name": "constant.numeric.isabelle"
    95     },
    96     {
    97       "name": "string.quoted.double.isabelle",
    98       "begin": "\"",
    99       "beginCaptures": {
   100         "0": { "name": "punctuation.definition.string.begin.isabelle" }
   101       },
   102       "patterns": [
   103         {
   104           "match": "\\\\.",
   105           "name": "constant.character.escape.isabelle"
   106         }
   107       ],
   108       "end": "\"",
   109       "endCaptures": {
   110         "0": { "name": "punctuation.definition.string.end.isabelle" }
   111       }
   112     }
   113   ]
   114 }
   115 """
   116   }
   117 
   118 
   119   /* Isabelle tool wrapper */
   120 
   121   val isabelle_tool = Isabelle_Tool("vscode_grammar",
   122     "generate static TextMate grammar for VSCode editor", args =>
   123   {
   124     var dirs: List[Path] = Nil
   125     var logic = default_logic
   126     var output: Option[Path] = None
   127 
   128     val getopts = Getopts("""
   129 Usage: isabelle vscode_grammar [OPTIONS]
   130 
   131   Options are:
   132     -d DIR       include session directory
   133     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
   134     -o FILE      output file name (default """ + default_output() + """)
   135 
   136   Generate static TextMate grammar for VSCode editor.
   137 """,
   138       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   139       "l:" -> (arg => logic = arg),
   140       "o:" -> (arg => output = Some(Path.explode(arg))))
   141 
   142     val more_args = getopts(args)
   143     if (more_args.nonEmpty) getopts.usage()
   144 
   145     val keywords = Build.outer_syntax(Options.init(), dirs, logic).keywords
   146     val output_path = output getOrElse Path.explode(default_output(logic))
   147 
   148     Output.writeln(output_path.implode)
   149     File.write_backup(output_path, generate(keywords))
   150   })
   151 }