src/Tools/VSCode/src/grammar.scala
author wenzelm
Sun Jan 01 23:19:34 2017 +0100 (2017-01-01)
changeset 64738 bcdecd466cb2
child 64739 3224021893c0
permissions -rw-r--r--
generate static TextMate grammar for VSCode editor;
     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 
    13 object Grammar
    14 {
    15   /* generate grammar */
    16 
    17   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    18 
    19   private def default_output(logic: String = ""): String =
    20     if (logic == default_logic) "isabelle-grammar.json"
    21     else "isabelle-" + logic + "-grammar.json"
    22 
    23   def generate(
    24     options: Options,
    25     session_dirs: List[Path] = Nil,
    26     session_name: String = default_logic,
    27     output: Path = Path.explode(default_output()))
    28   {
    29     val keywords = Build.outer_syntax(options, session_dirs, session_name).keywords
    30 
    31     val (minor_keywords, operators) =
    32       keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier(_))
    33 
    34     def major_keywords(pred: String => Boolean): List[String] =
    35       (for {
    36         k <- keywords.major.iterator
    37         kind <- keywords.kinds.get(k)
    38         if pred(kind)
    39       } yield k).toList
    40 
    41     val keywords1 =
    42       major_keywords(k => k != Keyword.THY_END && k != Keyword.PRF_ASM && k != Keyword.PRF_ASM_GOAL)
    43     val keywords2 = major_keywords(Set(Keyword.THY_END))
    44     val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL))
    45 
    46 
    47     def quote_name(a: String): String =
    48       if (Symbol.is_ascii_identifier(a)) a else "\\Q" + a + "\\E"
    49 
    50     def grouped_names(as: List[String]): String =
    51       JSON.Format("\\b(" + as.sorted.map(quote_name(_)).mkString("|") + ")\\b")
    52 
    53     File.write(output, """{
    54   "name": "Isabelle",
    55   "scopeName": "source.isabelle",
    56   "fileTypes": ["thy"],
    57   "uuid": "fb16e918-d05b-11e6-918e-2bb94aa2c605",
    58   "repository": {
    59     "comments": {
    60       "patterns": [
    61         {
    62           "name": "comment.block.isabelle",
    63           "begin": "\\(\\*",
    64           "beginCaptures": {
    65             "0": { "name": "punctuation.definition.comment.begin.isabelle" }
    66           },
    67           "patterns": [{ "include": "#comments" }],
    68           "end": "\\*\\)",
    69           "endCaptures": {
    70             "0": { "name": "punctuation.definition.comment.end.isabelle" }
    71           }
    72         }
    73       ]
    74     }
    75   },
    76   "patterns": [
    77     {
    78       "include": "#comments"
    79     },
    80     {
    81       "name": "keyword.control.isabelle",
    82       "match": """ + grouped_names(keywords1) + """
    83     },
    84     {
    85       "name": "keyword.other.isabelle",
    86       "match": """ + grouped_names(keywords2) + """
    87     },
    88     {
    89       "name": "keyword.operator.isabelle",
    90       "match": """ + grouped_names(operators) + """
    91     },
    92     {
    93       "name": "constant.language.isabelle",
    94       "match": """ + grouped_names(keywords3) + """
    95     },
    96     {
    97       "match": "\\b\\d*\\.?\\d+\\b",
    98       "name": "constant.numeric.isabelle"
    99     },
   100     {
   101       "name": "string.quoted.double.isabelle",
   102       "begin": "\"",
   103       "beginCaptures": {
   104         "0": { "name": "punctuation.definition.string.begin.isabelle" }
   105       },
   106       "patterns": [
   107         {
   108           "match": "\\\\.",
   109           "name": "constant.character.escape.isabelle"
   110         }
   111       ],
   112       "end": "\"",
   113       "endCaptures": {
   114         "0": { "name": "punctuation.definition.string.end.isabelle" }
   115       }
   116     }
   117   ]
   118 }
   119 """)
   120   }
   121 
   122 
   123   /* Isabelle tool wrapper */
   124 
   125   val isabelle_tool = Isabelle_Tool("vscode_grammar",
   126     "generate static TextMate grammar for VSCode editor", args =>
   127   {
   128     var dirs: List[Path] = Nil
   129     var logic = default_logic
   130     var output: Option[Path] = None
   131 
   132     val getopts = Getopts("""
   133 Usage: isabelle vscode_grammar [OPTIONS]
   134 
   135   Options are:
   136     -d DIR       include session directory
   137     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
   138     -o FILE      output file name (default """ + default_output() + """)
   139 
   140   Generate static TextMate grammar for VSCode editor.
   141 """,
   142       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   143       "l:" -> (arg => logic = arg),
   144       "o:" -> (arg => output = Some(Path.explode(arg))))
   145 
   146     val more_args = getopts(args)
   147     if (more_args.nonEmpty) getopts.usage()
   148 
   149     val output_path = output getOrElse Path.explode(default_output(logic))
   150     Output.writeln(output_path.implode)
   151 
   152     generate(Options.init(), dirs, logic, output_path)
   153   })
   154 }