author | wenzelm |
Wed, 11 May 2022 10:42:24 +0200 | |
changeset 75454 | 295e1c9d2994 |
parent 75394 | 42267c650205 |
child 77208 | a3f67a4459e1 |
permissions | -rw-r--r-- |
75292 | 1 |
/* Title: Tools/VSCode/src/vscode_main.scala |
75083 | 2 |
Author: Makarius |
3 |
||
75292 | 4 |
Main application entry point for Isabelle/VSCode. |
75083 | 5 |
*/ |
6 |
||
7 |
package isabelle.vscode |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
75315 | 12 |
import java.util.zip.ZipFile |
13 |
||
75083 | 14 |
|
75393 | 15 |
object VSCode_Main { |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
16 |
/* vscodium command-line interface */ |
75292 | 17 |
|
75298 | 18 |
def server_log_path: Path = |
19 |
Path.explode("$ISABELLE_VSCODE_SETTINGS/server.log").expand |
|
20 |
||
75304 | 21 |
def run_vscodium(args: List[String], |
75454 | 22 |
environment: List[(String, String)] = Nil, |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
23 |
options: List[String] = Nil, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
24 |
logic: String = "", |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
25 |
logic_ancestor: String = "", |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
26 |
logic_requirements: Boolean = false, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
27 |
session_dirs: List[Path] = Nil, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
28 |
include_sessions: List[String] = Nil, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
29 |
modes: List[String] = Nil, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
30 |
no_build: Boolean = false, |
75298 | 31 |
server_log: Boolean = false, |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
32 |
verbose: Boolean = false, |
75292 | 33 |
background: Boolean = false, |
75393 | 34 |
progress: Progress = new Progress |
35 |
): Process_Result = { |
|
75311 | 36 |
def platform_path(s: String): String = File.platform_path(Path.explode(s)) |
37 |
||
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
38 |
val args_json = |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
39 |
JSON.optional("options" -> proper_list(options)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
40 |
JSON.optional("logic" -> proper_string(logic)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
41 |
JSON.optional("logic_ancestor" -> proper_string(logic_ancestor)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
42 |
JSON.optional("logic_requirements" -> proper_bool(logic_requirements)) ++ |
75297
fc4d07587695
more robust errors -- on foreground process instead of background server;
wenzelm
parents:
75296
diff
changeset
|
43 |
JSON.optional("session_dirs" -> |
fc4d07587695
more robust errors -- on foreground process instead of background server;
wenzelm
parents:
75296
diff
changeset
|
44 |
proper_list(session_dirs.map(dir => Sessions.check_session_dir(dir).absolute.implode))) ++ |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
45 |
JSON.optional("include_sessions" -> proper_list(include_sessions)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
46 |
JSON.optional("modes" -> proper_list(modes)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
47 |
JSON.optional("no_build" -> proper_bool(no_build)) ++ |
75298 | 48 |
JSON.optional("log_file" -> |
49 |
(if (server_log) Some(server_log_path.absolute.implode) else None)) ++ |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
50 |
JSON.optional("verbose" -> proper_bool(verbose)) |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
51 |
|
75454 | 52 |
val env = |
53 |
Isabelle_System.settings(environment ::: List( |
|
54 |
"ISABELLE_VSCODIUM_ARGS" -> JSON.Format(args_json), |
|
55 |
"ISABELLE_VSCODIUM_APP" -> platform_path("$ISABELLE_VSCODIUM_RESOURCES/vscodium"), |
|
56 |
"ELECTRON_RUN_AS_NODE" -> "1")) |
|
75083 | 57 |
|
75292 | 58 |
val electron = Isabelle_System.getenv("ISABELLE_VSCODIUM_ELECTRON") |
59 |
if (electron.isEmpty) { |
|
60 |
error("""Undefined $ISABELLE_VSCODIUM_ELECTRON: missing "vscodium" component""") |
|
61 |
} |
|
62 |
val args0 = |
|
63 |
List(platform_path("$ISABELLE_VSCODIUM_RESOURCES/vscodium/out/cli.js"), |
|
64 |
"--ms-enable-electron-run-as-node", "--locale", "en-US", |
|
65 |
"--user-data-dir", platform_path("$ISABELLE_VSCODE_SETTINGS/user-data"), |
|
66 |
"--extensions-dir", platform_path("$ISABELLE_VSCODE_SETTINGS/extensions")) |
|
67 |
val script = |
|
68 |
Bash.strings(electron :: args0 ::: args) + |
|
69 |
(if (background) " > /dev/null 2> /dev/null &" else "") |
|
70 |
||
75293
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
71 |
progress.bash(script, env = env, echo = true) |
75292 | 72 |
} |
73 |
||
74 |
||
75312
e641ac92b489
more formal extension_manifest, with shasum for sources;
wenzelm
parents:
75311
diff
changeset
|
75 |
/* extension */ |
e641ac92b489
more formal extension_manifest, with shasum for sources;
wenzelm
parents:
75311
diff
changeset
|
76 |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
77 |
def default_vsix_path: Path = Path.explode("$ISABELLE_VSCODE_VSIX") |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
78 |
|
75312
e641ac92b489
more formal extension_manifest, with shasum for sources;
wenzelm
parents:
75311
diff
changeset
|
79 |
def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension") |
75334 | 80 |
val extension_name: String = "isabelle.isabelle" |
75312
e641ac92b489
more formal extension_manifest, with shasum for sources;
wenzelm
parents:
75311
diff
changeset
|
81 |
|
75348 | 82 |
val MANIFEST: Path = Path.explode("MANIFEST") |
75305 | 83 |
|
75393 | 84 |
private def shasum_vsix(vsix_path: Path): String = { |
75334 | 85 |
val name = "extension/MANIFEST.shasum" |
86 |
def err(): Nothing = error("Cannot retrieve " + quote(name) + " from " + vsix_path) |
|
87 |
if (vsix_path.is_file) { |
|
88 |
using(new ZipFile(vsix_path.file))(zip_file => |
|
89 |
zip_file.getEntry(name) match { |
|
90 |
case null => err() |
|
91 |
case entry => |
|
92 |
zip_file.getInputStream(entry) match { |
|
93 |
case null => err() |
|
94 |
case stream => File.read_stream(stream) |
|
95 |
} |
|
96 |
}) |
|
97 |
} |
|
98 |
else err() |
|
99 |
} |
|
100 |
||
75393 | 101 |
private def shasum_dir(dir: Path): Option[String] = { |
75334 | 102 |
val path = dir + MANIFEST.shasum |
103 |
if (path.is_file) Some(File.read(path)) else None |
|
104 |
} |
|
105 |
||
75393 | 106 |
def locate_extension(): Option[Path] = { |
75313 | 107 |
val out = run_vscodium(List("--locate-extension", extension_name)).check.out |
108 |
if (out.nonEmpty) Some(Path.explode(File.standard_path(out))) else None |
|
109 |
} |
|
110 |
||
75305 | 111 |
def uninstall_extension(progress: Progress = new Progress): Unit = |
75313 | 112 |
locate_extension() match { |
75332 | 113 |
case None => progress.echo_warning("No Isabelle/VSCode extension to uninstall") |
75313 | 114 |
case Some(dir) => |
115 |
run_vscodium(List("--uninstall-extension", extension_name)).check |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
116 |
progress.echo("Uninstalled Isabelle/VSCode extension from directory:\n" + dir) |
75313 | 117 |
} |
75305 | 118 |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
119 |
def install_extension( |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
120 |
vsix_path: Path = default_vsix_path, |
75393 | 121 |
progress: Progress = new Progress |
122 |
): Unit = { |
|
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
123 |
val new_shasum = shasum_vsix(vsix_path) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
124 |
val old_shasum = locate_extension().flatMap(shasum_dir) |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
125 |
val current = old_shasum.isDefined && old_shasum.get == new_shasum |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
126 |
|
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
127 |
if (!current) { |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
128 |
run_vscodium(List("--install-extension", File.bash_platform_path(vsix_path))).check |
75313 | 129 |
locate_extension() match { |
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
130 |
case None => error("Missing Isabelle/VSCode extension after installation") |
75313 | 131 |
case Some(dir) => |
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
132 |
progress.echo("Installed Isabelle/VSCode extension " + vsix_path.expand + |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
133 |
"\ninto directory: " + dir) |
75313 | 134 |
} |
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
135 |
} |
75305 | 136 |
} |
137 |
||
138 |
||
75292 | 139 |
/* settings */ |
140 |
||
141 |
def settings_path: Path = |
|
75257
d1e5f9dbf885
clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode;
wenzelm
parents:
75252
diff
changeset
|
142 |
Path.explode("$ISABELLE_VSCODE_SETTINGS/user-data/User/settings.json") |
75083 | 143 |
|
75292 | 144 |
private val default_settings = """ { |
75166 | 145 |
"editor.fontFamily": "'Isabelle DejaVu Sans Mono'", |
146 |
"editor.fontSize": 18, |
|
147 |
"editor.lineNumbers": "off", |
|
148 |
"editor.renderIndentGuides": false, |
|
149 |
"editor.rulers": [80, 100], |
|
75171 | 150 |
"editor.unicodeHighlight.ambiguousCharacters": false, |
75166 | 151 |
"extensions.autoCheckUpdates": false, |
75167 | 152 |
"extensions.autoUpdate": false, |
75178 | 153 |
"terminal.integrated.fontFamily": "monospace", |
75167 | 154 |
"update.mode": "none" |
75166 | 155 |
} |
156 |
""" |
|
157 |
||
75393 | 158 |
def init_settings(): Unit = { |
75292 | 159 |
if (!settings_path.is_file) { |
160 |
Isabelle_System.make_directory(settings_path.dir) |
|
161 |
File.write(settings_path, default_settings) |
|
75163 | 162 |
} |
75083 | 163 |
} |
164 |
||
165 |
||
166 |
/* Isabelle tool wrapper */ |
|
167 |
||
168 |
val isabelle_tool = |
|
75393 | 169 |
Isabelle_Tool("vscode", "Isabelle/VSCode interface wrapper", Scala_Project.here, |
75394 | 170 |
{ args => |
171 |
var logic_ancestor = "" |
|
172 |
var console = false |
|
173 |
var edit_extension = false |
|
174 |
var server_log = false |
|
175 |
var logic_requirements = false |
|
176 |
var uninstall = false |
|
177 |
var vsix_path = default_vsix_path |
|
178 |
var session_dirs = List.empty[Path] |
|
179 |
var include_sessions = List.empty[String] |
|
180 |
var logic = "" |
|
181 |
var modes = List.empty[String] |
|
182 |
var no_build = false |
|
183 |
var options = List.empty[String] |
|
184 |
var verbose = false |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
185 |
|
75394 | 186 |
def add_option(opt: String): Unit = options = options ::: List(opt) |
75293
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
187 |
|
75394 | 188 |
val getopts = Getopts(""" |
75316 | 189 |
Usage: isabelle vscode [OPTIONS] [ARGUMENTS] [-- VSCODE_OPTIONS] |
75293
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
190 |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
191 |
-A NAME ancestor session for option -R (default: parent) |
75293
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
192 |
-C run as foreground process, with console output |
75332 | 193 |
-E edit Isabelle/VSCode extension project sources |
75298 | 194 |
-L enable language server log to file: |
195 |
""" + server_log_path.implode + """ |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
196 |
-R NAME build image with requirements from other sessions |
75332 | 197 |
-U uninstall Isabelle/VSCode extension |
75333
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
198 |
-V FILE specify VSIX file for Isabelle/VSCode extension |
8f0d94fb8551
provide vscode_extension via component, thus users don't need Node.js development tools;
wenzelm
parents:
75332
diff
changeset
|
199 |
(default: """ + default_vsix_path + """) |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
200 |
-d DIR include session directory |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
201 |
-i NAME include session in name-space of theories |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
202 |
-l NAME logic session name |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
203 |
-m MODE add print mode for output |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
204 |
-n no build of session image on startup |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
205 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
206 |
-p CMD ML process command prefix (process policy) |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
207 |
-s system build mode for session image (system_heaps=true) |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
208 |
-u user build mode for session image (system_heaps=false) |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
209 |
-v verbose logging of language server |
75083 | 210 |
|
75292 | 211 |
Start Isabelle/VSCode application, with automatic configuration of |
212 |
user settings. |
|
75163 | 213 |
|
214 |
The following initial settings are provided for a fresh installation: |
|
75293
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
215 |
""" + default_settings, |
75394 | 216 |
"A:" -> (arg => logic_ancestor = arg), |
217 |
"C" -> (_ => console = true), |
|
218 |
"E" -> (_ => edit_extension = true), |
|
219 |
"L" -> (_ => server_log = true), |
|
220 |
"R:" -> (arg => { logic = arg; logic_requirements = true }), |
|
221 |
"U" -> (_ => uninstall = true), |
|
222 |
"V:" -> (arg => vsix_path = Path.explode(arg)), |
|
223 |
"d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))), |
|
224 |
"i:" -> (arg => include_sessions = include_sessions ::: List(arg)), |
|
225 |
"l:" -> (arg => { logic = arg; logic_requirements = false }), |
|
226 |
"m:" -> (arg => modes = modes ::: List(arg)), |
|
227 |
"n" -> (_ => no_build = true), |
|
228 |
"o:" -> add_option, |
|
229 |
"p:" -> (arg => add_option("ML_process_policy=" + arg)), |
|
230 |
"s" -> (_ => add_option("system_heaps=true")), |
|
231 |
"u" -> (_ => add_option("system_heaps=false")), |
|
232 |
"v" -> (_ => verbose = true)) |
|
75083 | 233 |
|
75394 | 234 |
val more_args = getopts(args) |
75292 | 235 |
|
75394 | 236 |
init_settings() |
75083 | 237 |
|
75394 | 238 |
val console_progress = new Console_Progress |
75332 | 239 |
|
75394 | 240 |
if (uninstall) uninstall_extension(progress = console_progress) |
241 |
else install_extension(vsix_path = vsix_path, progress = console_progress) |
|
75332 | 242 |
|
75394 | 243 |
val (background, app_progress) = |
244 |
if (console) (false, console_progress) |
|
245 |
else { run_vscodium(List("--version")).check; (true, new Progress) } |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
246 |
|
75394 | 247 |
run_vscodium( |
248 |
more_args ::: (if (edit_extension) List(File.platform_path(extension_dir)) else Nil), |
|
249 |
options = options, logic = logic, logic_ancestor = logic_ancestor, |
|
250 |
logic_requirements = logic_requirements, session_dirs = session_dirs, |
|
251 |
include_sessions = include_sessions, modes = modes, no_build = no_build, |
|
252 |
server_log = server_log, verbose = verbose, background = background, |
|
253 |
progress = app_progress).check |
|
254 |
}) |
|
75083 | 255 |
} |