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