1 /* Title: Tools/VSCode/src/textmate_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 TextMate_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().toString) + """, |
|
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", Scala_Project.here, args => |
|
138 { |
|
139 var dirs: List[Path] = Nil |
|
140 var logic = default_logic |
|
141 var output: Option[Path] = None |
|
142 |
|
143 val getopts = Getopts(""" |
|
144 Usage: 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 } |
|