author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 75348 | 583ad7a9941c |
child 75394 | 42267c650205 |
permissions | -rw-r--r-- |
75254 | 1 |
/* Title: Tools/VSCode/src/build_vscode_extension.scala |
65138 | 2 |
Author: Makarius |
3 |
||
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
4 |
Build the Isabelle/VSCode extension as component. |
65138 | 5 |
*/ |
6 |
||
7 |
package isabelle.vscode |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
||
75393 | 13 |
object Build_VSCode { |
75289
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
14 |
/* build grammar */ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
15 |
|
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
16 |
def default_logic: String = Isabelle_System.getenv("ISABELLE_LOGIC") |
65138 | 17 |
|
75290
c9ee3028c125
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
wenzelm
parents:
75289
diff
changeset
|
18 |
def build_grammar(options: Options, build_dir: Path, |
75289
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
19 |
logic: String = default_logic, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
20 |
dirs: List[Path] = Nil, |
75393 | 21 |
progress: Progress = new Progress |
22 |
): Unit = { |
|
75289
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
23 |
val keywords = |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
24 |
Sessions.base_info(options, logic, dirs = dirs).check.base.overall_syntax.keywords |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
25 |
|
75290
c9ee3028c125
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
wenzelm
parents:
75289
diff
changeset
|
26 |
val output_path = build_dir + Path.explode("isabelle-grammar.json") |
75289
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
27 |
progress.echo(output_path.expand.implode) |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
28 |
|
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
29 |
val (minor_keywords, operators) = |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
30 |
keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier) |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
31 |
|
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
32 |
def major_keywords(pred: String => Boolean): List[String] = |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
33 |
(for { |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
34 |
k <- keywords.major.iterator |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
35 |
kind <- keywords.kinds.get(k) |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
36 |
if pred(kind) |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
37 |
} yield k).toList |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
38 |
|
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
39 |
val keywords1 = |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
40 |
major_keywords(k => k != Keyword.THY_END && k != Keyword.PRF_ASM && k != Keyword.PRF_ASM_GOAL) |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
41 |
val keywords2 = minor_keywords ::: major_keywords(Set(Keyword.THY_END)) |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
42 |
val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL)) |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
43 |
|
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
44 |
def grouped_names(as: List[String]): String = |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
45 |
JSON.Format("\\b(" + as.sorted.map(Library.escape_regex).mkString("|") + ")\\b") |
65138 | 46 |
|
75289
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
47 |
File.write_backup(output_path, """{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
48 |
"name": "Isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
49 |
"scopeName": "source.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
50 |
"fileTypes": ["thy"], |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
51 |
"uuid": """ + JSON.Format(UUID.random().toString) + """, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
52 |
"repository": { |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
53 |
"comment": { |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
54 |
"patterns": [ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
55 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
56 |
"name": "comment.block.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
57 |
"begin": "\\(\\*", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
58 |
"patterns": [{ "include": "#comment" }], |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
59 |
"end": "\\*\\)" |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
60 |
} |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
61 |
] |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
62 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
63 |
"cartouche": { |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
64 |
"patterns": [ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
65 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
66 |
"name": "string.quoted.other.multiline.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
67 |
"begin": "(?:\\\\<open>|‹)", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
68 |
"patterns": [{ "include": "#cartouche" }], |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
69 |
"end": "(?:\\\\<close>|›)" |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
70 |
} |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
71 |
] |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
72 |
} |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
73 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
74 |
"patterns": [ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
75 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
76 |
"include": "#comment" |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
77 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
78 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
79 |
"include": "#cartouche" |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
80 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
81 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
82 |
"name": "keyword.control.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
83 |
"match": """ + grouped_names(keywords1) + """ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
84 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
85 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
86 |
"name": "keyword.other.unit.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
87 |
"match": """ + grouped_names(keywords2) + """ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
88 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
89 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
90 |
"name": "keyword.operator.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
91 |
"match": """ + grouped_names(operators) + """ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
92 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
93 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
94 |
"name": "entity.name.type.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
95 |
"match": """ + grouped_names(keywords3) + """ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
96 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
97 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
98 |
"name": "constant.numeric.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
99 |
"match": "\\b\\d*\\.?\\d+\\b" |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
100 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
101 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
102 |
"name": "string.quoted.double.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
103 |
"begin": "\"", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
104 |
"patterns": [ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
105 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
106 |
"name": "constant.character.escape.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
107 |
"match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
108 |
} |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
109 |
], |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
110 |
"end": "\"" |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
111 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
112 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
113 |
"name": "string.quoted.backtick.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
114 |
"begin": "`", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
115 |
"patterns": [ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
116 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
117 |
"name": "constant.character.escape.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
118 |
"match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
119 |
} |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
120 |
], |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
121 |
"end": "`" |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
122 |
}, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
123 |
{ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
124 |
"name": "string.quoted.verbatim.isabelle", |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
125 |
"begin": """ + JSON.Format("""\{\*""") + """, |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
126 |
"patterns": [ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
127 |
{ "match": """ + JSON.Format("""[^*]+|\*(?!\})""") + """ } |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
128 |
], |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
129 |
"end": """ + JSON.Format("""\*\}""") + """ |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
130 |
} |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
131 |
] |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
132 |
} |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
133 |
""") |
65138 | 134 |
} |
135 |
||
136 |
||
75312
e641ac92b489
more formal extension_manifest, with shasum for sources;
wenzelm
parents:
75306
diff
changeset
|
137 |
/* build extension */ |
75290
c9ee3028c125
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
wenzelm
parents:
75289
diff
changeset
|
138 |
|
c9ee3028c125
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
wenzelm
parents:
75289
diff
changeset
|
139 |
def build_extension(options: Options, |
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
140 |
target_dir: Path = Path.current, |
75290
c9ee3028c125
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
wenzelm
parents:
75289
diff
changeset
|
141 |
logic: String = default_logic, |
c9ee3028c125
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
wenzelm
parents:
75289
diff
changeset
|
142 |
dirs: List[Path] = Nil, |
75393 | 143 |
progress: Progress = new Progress |
144 |
): Unit = { |
|
75259 | 145 |
Isabelle_System.require_command("node") |
146 |
Isabelle_System.require_command("yarn") |
|
147 |
Isabelle_System.require_command("vsce") |
|
148 |
||
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
149 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
150 |
/* component */ |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
151 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
152 |
val component_name = "vscode_extension-" + Date.Format.alt_date(Date.now()) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
153 |
val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name)) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
154 |
progress.echo("Component " + component_dir) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
155 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
156 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
157 |
/* build */ |
65138 | 158 |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
159 |
val vsix_name = |
75393 | 160 |
Isabelle_System.with_tmp_dir("build")(build_dir => { |
75348 | 161 |
val manifest_text = File.read(VSCode_Main.extension_dir + VSCode_Main.MANIFEST) |
162 |
val manifest_entries = split_lines(manifest_text).filter(_.nonEmpty) |
|
75393 | 163 |
val manifest_shasum: String = { |
75348 | 164 |
val a = SHA1.digest(manifest_text).shasum("<MANIFEST>") |
165 |
val bs = |
|
166 |
for (entry <- manifest_entries) |
|
167 |
yield SHA1.digest(VSCode_Main.extension_dir + Path.explode(entry)).shasum(entry) |
|
168 |
terminate_lines(a :: bs) |
|
169 |
} |
|
170 |
for (entry <- manifest_entries) { |
|
171 |
val path = Path.explode(entry) |
|
172 |
Isabelle_System.copy_file(VSCode_Main.extension_dir + path, |
|
173 |
Isabelle_System.make_directory(build_dir + path.dir)) |
|
174 |
} |
|
175 |
File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum) |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
176 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
177 |
build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
178 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
179 |
val result = |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
180 |
progress.bash("yarn && vsce package", cwd = build_dir.file, echo = true).check |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
181 |
val Pattern = """.*Packaged:.*(isabelle-.*\.vsix).*""".r |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
182 |
val vsix_name = |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
183 |
result.out_lines.collectFirst({ case Pattern(name) => name }) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
184 |
.getOrElse(error("Failed to guess resulting .vsix file name")) |
75143 | 185 |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
186 |
Isabelle_System.copy_file(build_dir + Path.basic(vsix_name), component_dir) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
187 |
vsix_name |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
188 |
}) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
189 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
190 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
191 |
/* settings */ |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
192 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
193 |
val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
194 |
File.write(etc_dir + Path.basic("settings"), |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
195 |
"""# -*- shell-script -*- :mode=shellscript: |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
196 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
197 |
ISABELLE_VSCODE_VSIX="$COMPONENT/""" + vsix_name + "\"\n") |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
198 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
199 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
200 |
/* README */ |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
201 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
202 |
File.write(component_dir + Path.basic("README"), |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
203 |
"""This the Isabelle/VSCode extension as VSIX package |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
204 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
205 |
It has been produced from the sources in $ISABELLE_HOME/src/Tools/extension/. |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
206 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
207 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
208 |
Makarius |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
209 |
""" + Date.Format.date(Date.now()) + "\n") |
65138 | 210 |
} |
211 |
||
212 |
||
213 |
/* Isabelle tool wrapper */ |
|
214 |
||
215 |
val isabelle_tool = |
|
75254 | 216 |
Isabelle_Tool("build_vscode_extension", "build Isabelle/VSCode extension module", |
75393 | 217 |
Scala_Project.here, |
218 |
args => { |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
219 |
var target_dir = Path.current |
75289
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
220 |
var dirs: List[Path] = Nil |
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
221 |
var logic = default_logic |
65138 | 222 |
|
223 |
val getopts = Getopts(""" |
|
75254 | 224 |
Usage: isabelle build_vscode_extension |
65138 | 225 |
|
226 |
Options are: |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
227 |
-D DIR target directory (default ".") |
75290
c9ee3028c125
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
wenzelm
parents:
75289
diff
changeset
|
228 |
-d DIR include session directory |
75289
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
229 |
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) |
65138 | 230 |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
231 |
Build the Isabelle/VSCode extension as component, for inclusion into the |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
232 |
local VSCodium configuration. |
65138 | 233 |
""", |
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
234 |
"D:" -> (arg => target_dir = Path.explode(arg)), |
75289
9c72957e5c4a
incorporate build_grammar into build_vscode_extension;
wenzelm
parents:
75281
diff
changeset
|
235 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
75290
c9ee3028c125
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
wenzelm
parents:
75289
diff
changeset
|
236 |
"l:" -> (arg => logic = arg)) |
65138 | 237 |
|
238 |
val more_args = getopts(args) |
|
239 |
if (more_args.nonEmpty) getopts.usage() |
|
240 |
||
241 |
val options = Options.init() |
|
242 |
val progress = new Console_Progress() |
|
243 |
||
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
244 |
build_extension(options, target_dir = target_dir, logic = logic, dirs = dirs, |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
245 |
progress = progress) |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
66976
diff
changeset
|
246 |
}) |
65138 | 247 |
} |