author | wenzelm |
Tue, 22 Mar 2022 18:56:28 +0100 | |
changeset 75297 | fc4d07587695 |
parent 75296 | d92e0197ba01 |
child 75298 | 064e44da2e88 |
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 |
||
12 |
||
75292 | 13 |
object VSCode_Main |
75083 | 14 |
{ |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
15 |
/* vscodium command-line interface */ |
75292 | 16 |
|
17 |
private def platform_path(s: String): String = File.platform_path(Path.explode(s)) |
|
18 |
||
19 |
def run_cli(args: List[String], |
|
20 |
environment: Iterable[(String, String)] = Nil, |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
21 |
options: List[String] = Nil, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
22 |
logic: String = "", |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
23 |
logic_ancestor: String = "", |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
24 |
logic_requirements: Boolean = false, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
25 |
session_dirs: List[Path] = Nil, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
26 |
include_sessions: List[String] = Nil, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
27 |
modes: List[String] = Nil, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
28 |
no_build: Boolean = false, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
29 |
log_file: Option[Path] = None, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
30 |
verbose: Boolean = false, |
75292 | 31 |
background: Boolean = false, |
32 |
progress: Progress = new Progress): Process_Result = |
|
33 |
{ |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
34 |
val args_json = |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
35 |
JSON.optional("options" -> proper_list(options)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
36 |
JSON.optional("logic" -> proper_string(logic)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
37 |
JSON.optional("logic_ancestor" -> proper_string(logic_ancestor)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
38 |
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
|
39 |
JSON.optional("session_dirs" -> |
fc4d07587695
more robust errors -- on foreground process instead of background server;
wenzelm
parents:
75296
diff
changeset
|
40 |
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
|
41 |
JSON.optional("include_sessions" -> proper_list(include_sessions)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
42 |
JSON.optional("modes" -> proper_list(modes)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
43 |
JSON.optional("no_build" -> proper_bool(no_build)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
44 |
JSON.optional("log_file" -> log_file.map(_.absolute.implode)) ++ |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
45 |
JSON.optional("verbose" -> proper_bool(verbose)) |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
46 |
|
75292 | 47 |
val env = new java.util.HashMap(Isabelle_System.settings()) |
48 |
for ((a, b) <- environment) env.put(a, b) |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
49 |
env.put("ISABELLE_VSCODIUM_ARGS", JSON.Format(args_json)) |
75292 | 50 |
env.put("ISABELLE_VSCODIUM_APP", platform_path("$ISABELLE_VSCODIUM_RESOURCES/vscodium")) |
51 |
env.put("ELECTRON_RUN_AS_NODE", "1") |
|
75083 | 52 |
|
75292 | 53 |
val electron = Isabelle_System.getenv("ISABELLE_VSCODIUM_ELECTRON") |
54 |
if (electron.isEmpty) { |
|
55 |
error("""Undefined $ISABELLE_VSCODIUM_ELECTRON: missing "vscodium" component""") |
|
56 |
} |
|
57 |
val args0 = |
|
58 |
List(platform_path("$ISABELLE_VSCODIUM_RESOURCES/vscodium/out/cli.js"), |
|
59 |
"--ms-enable-electron-run-as-node", "--locale", "en-US", |
|
60 |
"--user-data-dir", platform_path("$ISABELLE_VSCODE_SETTINGS/user-data"), |
|
61 |
"--extensions-dir", platform_path("$ISABELLE_VSCODE_SETTINGS/extensions")) |
|
62 |
val script = |
|
63 |
Bash.strings(electron :: args0 ::: args) + |
|
64 |
(if (background) " > /dev/null 2> /dev/null &" else "") |
|
65 |
||
75293
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
66 |
progress.bash(script, env = env, echo = true) |
75292 | 67 |
} |
68 |
||
69 |
||
70 |
/* settings */ |
|
71 |
||
72 |
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
|
73 |
Path.explode("$ISABELLE_VSCODE_SETTINGS/user-data/User/settings.json") |
75083 | 74 |
|
75292 | 75 |
private val default_settings = """ { |
75166 | 76 |
"editor.fontFamily": "'Isabelle DejaVu Sans Mono'", |
77 |
"editor.fontSize": 18, |
|
78 |
"editor.lineNumbers": "off", |
|
79 |
"editor.renderIndentGuides": false, |
|
80 |
"editor.rulers": [80, 100], |
|
75171 | 81 |
"editor.unicodeHighlight.ambiguousCharacters": false, |
75166 | 82 |
"extensions.autoCheckUpdates": false, |
75167 | 83 |
"extensions.autoUpdate": false, |
75178 | 84 |
"terminal.integrated.fontFamily": "monospace", |
75167 | 85 |
"update.mode": "none" |
75166 | 86 |
} |
87 |
""" |
|
88 |
||
75292 | 89 |
def init_settings(): Unit = |
75083 | 90 |
{ |
75292 | 91 |
if (!settings_path.is_file) { |
92 |
Isabelle_System.make_directory(settings_path.dir) |
|
93 |
File.write(settings_path, default_settings) |
|
75163 | 94 |
} |
75083 | 95 |
} |
96 |
||
97 |
||
98 |
/* Isabelle tool wrapper */ |
|
99 |
||
100 |
val isabelle_tool = |
|
75292 | 101 |
Isabelle_Tool("vscode", "Isabelle/VSCode interface wrapper", Scala_Project.here, args => |
75083 | 102 |
{ |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
103 |
var logic_ancestor = "" |
75293
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
104 |
var console = false |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
105 |
var log_file: Option[Path] = None |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
106 |
var logic_requirements = false |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
107 |
var session_dirs = List.empty[Path] |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
108 |
var include_sessions = List.empty[String] |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
109 |
var logic = "" |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
110 |
var modes = List.empty[String] |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
111 |
var no_build = false |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
112 |
var options = List.empty[String] |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
113 |
var verbose = false |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
114 |
|
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
115 |
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
|
116 |
|
75083 | 117 |
val getopts = Getopts(""" |
75293
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
118 |
Usage: isabelle vscode [OPTIONS] [-- VSCODE_OPTIONS ...] |
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
119 |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
120 |
-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
|
121 |
-C run as foreground process, with console output |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
122 |
-L FILE logging on FILE |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
123 |
-R NAME build image with requirements from other sessions |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
124 |
-d DIR include session directory |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
125 |
-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
|
126 |
-l NAME logic session name |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
127 |
-m MODE add print mode for output |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
128 |
-n no build of session image on startup |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
129 |
-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
|
130 |
-p CMD ML process command prefix (process policy) |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
131 |
-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
|
132 |
-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
|
133 |
-v verbose logging of language server |
75083 | 134 |
|
75292 | 135 |
Start Isabelle/VSCode application, with automatic configuration of |
136 |
user settings. |
|
75163 | 137 |
|
138 |
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
|
139 |
""" + default_settings, |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
140 |
"A:" -> (arg => logic_ancestor = arg), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
141 |
"C" -> (_ => console = true), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
142 |
"L:" -> (arg => log_file = Some(Path.explode(arg))), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
143 |
"R:" -> (arg => { logic = arg; logic_requirements = true }), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
144 |
"d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
145 |
"i:" -> (arg => include_sessions = include_sessions ::: List(arg)), |
75296 | 146 |
"l:" -> (arg => { logic = arg; logic_requirements = false }), |
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
147 |
"m:" -> (arg => modes = modes ::: List(arg)), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
148 |
"n" -> (_ => no_build = true), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
149 |
"o:" -> add_option, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
150 |
"p:" -> (arg => add_option("ML_process_policy=" + arg)), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
151 |
"s" -> (_ => add_option("system_heaps=true")), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
152 |
"u" -> (_ => add_option("system_heaps=false")), |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
153 |
"v" -> (_ => verbose = true)) |
75083 | 154 |
|
155 |
val more_args = getopts(args) |
|
75292 | 156 |
|
75293
c5da08c5b01b
support console output, e.g. "isabelle vscode -C -- --help";
wenzelm
parents:
75292
diff
changeset
|
157 |
init_settings() |
75083 | 158 |
|
75295
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
159 |
val (background, progress) = |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
160 |
if (console) (false, new Console_Progress) |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
161 |
else { run_cli(List("--version")).check; (true, new Progress) } |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
162 |
|
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
163 |
run_cli(more_args, options = options, logic = logic, logic_ancestor = logic_ancestor, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
164 |
logic_requirements = logic_requirements, session_dirs = session_dirs, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
165 |
include_sessions = include_sessions, modes = modes, no_build = no_build, |
38398766be6b
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents:
75293
diff
changeset
|
166 |
log_file = log_file, verbose = verbose, background = background, progress = progress).check |
75083 | 167 |
}) |
168 |
} |