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