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