# HG changeset patch # User wenzelm # Date 1647969178 -3600 # Node ID 38398766be6be94b3b29e04acb98959c69da0ad4 # Parent 9004ded79add5bd9e4cb53cfbbd65495b963fe0a command-line arguments for "isabelle vscode", similar to "isabelle jedit"; diff -r 9004ded79add -r 38398766be6b src/Pure/ROOT.scala --- a/src/Pure/ROOT.scala Tue Mar 22 16:49:18 2022 +0100 +++ b/src/Pure/ROOT.scala Tue Mar 22 18:12:58 2022 +0100 @@ -18,6 +18,7 @@ val quote = Library.quote _ val commas = Library.commas _ val commas_quote = Library.commas_quote _ + val proper_bool = Library.proper_bool _ val proper_string = Library.proper_string _ def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list) } diff -r 9004ded79add -r 38398766be6b src/Pure/library.scala --- a/src/Pure/library.scala Tue Mar 22 16:49:18 2022 +0100 +++ b/src/Pure/library.scala Tue Mar 22 18:12:58 2022 +0100 @@ -280,6 +280,9 @@ /* proper values */ + def proper_bool(b: Boolean): Option[Boolean] = + if (!b) None else Some(b) + def proper_string(s: String): Option[String] = if (s == null || s == "") None else Some(s) diff -r 9004ded79add -r 38398766be6b src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Tue Mar 22 16:49:18 2022 +0100 +++ b/src/Tools/VSCode/extension/package.json Tue Mar 22 18:12:58 2022 +0100 @@ -193,14 +193,6 @@ "configuration": { "title": "Isabelle", "properties": { - "isabelle.args": { - "type": "array", - "items": { - "type": "string" - }, - "default": [], - "description": "Command-line arguments for isabelle vscode_server process." - }, "isabelle.replacement": { "type": "string", "default": "non-alphanumeric", diff -r 9004ded79add -r 38398766be6b src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Tue Mar 22 16:49:18 2022 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Tue Mar 22 18:12:58 2022 +0100 @@ -25,6 +25,63 @@ let last_caret_update: lsp.Caret_Update = {} + +/* command-line arguments from "isabelle vscode" */ + +interface Args +{ + options?: string[], + logic?: string, + logic_ancestor?: string, + logic_requirements?: boolean, + sesion_dirs?: string[], + include_sessions?: string[], + modes?: string[], + log_file?: string, + verbose?: boolean +} + +function print_value(x: any): string +{ + return typeof(x) === "string" ? x : JSON.stringify(x) +} + +function isabelle_options(args: Args): string[] +{ + var result: string[] = [] + function add(s: string) { result.push(s) } + function add_value(opt: string, slot: string) + { + const x = args[slot] + if (x) { add(opt); add(print_value(x)) } + } + function add_values(opt: string, slot: string) + { + const xs: any[] = args[slot] + if (xs) { + for (const x of xs) { add(opt); add(print_value(x)) } + } + } + + add("-o"); add("vscode_unicode_symbols") + add("-o"); add("vscode_pide_extensions") + add_values("-o", "options") + + add_value("-A", "logic_ancestor") + if (args.logic) { add_value(args.logic_requirements ? "-R" : "-l", "logic") } + + add_values("-d", "session_dirs") + add_values("-i", "include_sessions") + add_values("-m", "modes") + add_value("-L", "log_file") + if (args.verbose) { add("-v") } + + return result +} + + +/* activate extension */ + export async function activate(context: ExtensionContext) { /* server */ @@ -32,16 +89,15 @@ try { const isabelle_home = library.getenv_strict("ISABELLE_HOME") const isabelle_tool = isabelle_home + "/bin/isabelle" - const isabelle_args = - ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"] - .concat(vscode_lib.get_configuration>("args")) + const args = JSON.parse(library.getenv("ISABELLE_VSCODIUM_ARGS") || "{}") + const server_opts = isabelle_options(args) const server_options: ServerOptions = platform.is_windows() ? { command: file.cygwin_bash(), - args: ["-l", isabelle_tool, "vscode_server"].concat(isabelle_args) } : + args: ["-l", isabelle_tool, "vscode_server"].concat(server_opts) } : { command: isabelle_tool, - args: ["vscode_server"].concat(isabelle_args) } + args: ["vscode_server"].concat(server_opts) } const language_client_options: LanguageClientOptions = { documentSelector: [ diff -r 9004ded79add -r 38398766be6b src/Tools/VSCode/src/language_server.scala --- a/src/Tools/VSCode/src/language_server.scala Tue Mar 22 16:49:18 2022 +0100 +++ b/src/Tools/VSCode/src/language_server.scala Tue Mar 22 18:12:58 2022 +0100 @@ -39,6 +39,7 @@ var include_sessions: List[String] = Nil var logic = default_logic var modes: List[String] = Nil + var no_build = false var options = Options.init() var verbose = false @@ -53,6 +54,7 @@ -i NAME include session in name-space of theories -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) -m MODE add print mode for output + -n no build of session image on startup -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose logging @@ -65,6 +67,7 @@ "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), + "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true)) @@ -76,7 +79,8 @@ val server = new Language_Server(channel, options, session_name = logic, session_dirs = dirs, include_sessions = include_sessions, session_ancestor = logic_ancestor, - session_requirements = logic_requirements, modes = modes, log = log) + session_requirements = logic_requirements, session_no_build = no_build, + modes = modes, log = log) // prevent spurious garbage on the main protocol channel val orig_out = System.out @@ -103,6 +107,7 @@ session_dirs: List[Path] = Nil, session_ancestor: Option[String] = None, session_requirements: Boolean = false, + session_no_build: Boolean = false, modes: List[String] = Nil, log: Logger = No_Logger) { @@ -274,7 +279,7 @@ selection = Sessions.Selection.session(base_info.session), build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos) - if (!build(no_build = true).ok) { + if (!session_no_build && !build(no_build = true).ok) { val start_msg = "Build started for Isabelle/" + base_info.session + " ..." val fail_msg = "Session build failed -- prover process remains inactive!" diff -r 9004ded79add -r 38398766be6b src/Tools/VSCode/src/vscode_main.scala --- a/src/Tools/VSCode/src/vscode_main.scala Tue Mar 22 16:49:18 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_main.scala Tue Mar 22 18:12:58 2022 +0100 @@ -12,17 +12,40 @@ object VSCode_Main { - /* command-line interface */ + /* vscodium command-line interface */ private def platform_path(s: String): String = File.platform_path(Path.explode(s)) def run_cli(args: List[String], environment: Iterable[(String, String)] = Nil, + options: List[String] = Nil, + logic: String = "", + logic_ancestor: String = "", + logic_requirements: Boolean = false, + session_dirs: List[Path] = Nil, + include_sessions: List[String] = Nil, + modes: List[String] = Nil, + no_build: Boolean = false, + log_file: Option[Path] = None, + verbose: Boolean = false, background: Boolean = false, progress: Progress = new Progress): Process_Result = { + val args_json = + JSON.optional("options" -> proper_list(options)) ++ + JSON.optional("logic" -> proper_string(logic)) ++ + JSON.optional("logic_ancestor" -> proper_string(logic_ancestor)) ++ + JSON.optional("logic_requirements" -> proper_bool(logic_requirements)) ++ + JSON.optional("session_dirs" -> proper_list(session_dirs.map(_.absolute.implode))) ++ + JSON.optional("include_sessions" -> proper_list(include_sessions)) ++ + JSON.optional("modes" -> proper_list(modes)) ++ + JSON.optional("no_build" -> proper_bool(no_build)) ++ + JSON.optional("log_file" -> log_file.map(_.absolute.implode)) ++ + JSON.optional("verbose" -> proper_bool(verbose)) + val env = new java.util.HashMap(Isabelle_System.settings()) for ((a, b) <- environment) env.put(a, b) + env.put("ISABELLE_VSCODIUM_ARGS", JSON.Format(args_json)) env.put("ISABELLE_VSCODIUM_APP", platform_path("$ISABELLE_VSCODIUM_RESOURCES/vscodium")) env.put("ELECTRON_RUN_AS_NODE", "1") @@ -76,30 +99,69 @@ val isabelle_tool = Isabelle_Tool("vscode", "Isabelle/VSCode interface wrapper", Scala_Project.here, args => { + var logic_ancestor = "" var console = false + var log_file: Option[Path] = None + var logic_requirements = false + var session_dirs = List.empty[Path] + var include_sessions = List.empty[String] + var logic = "" + var modes = List.empty[String] + var no_build = false + var options = List.empty[String] + var verbose = false + + def add_option(opt: String): Unit = options = options ::: List(opt) val getopts = Getopts(""" Usage: isabelle vscode [OPTIONS] [-- VSCODE_OPTIONS ...] + -A NAME ancestor session for option -R (default: parent) -C run as foreground process, with console output + -L FILE logging on FILE + -R NAME build image with requirements from other sessions + -d DIR include session directory + -i NAME include session in name-space of theories + -l NAME logic session name + -m MODE add print mode for output + -n no build of session image on startup + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -p CMD ML process command prefix (process policy) + -s system build mode for session image (system_heaps=true) + -u user build mode for session image (system_heaps=false) + -v verbose logging of language server Start Isabelle/VSCode application, with automatic configuration of user settings. The following initial settings are provided for a fresh installation: """ + default_settings, - "C" -> (_ => console = true)) + "A:" -> (arg => logic_ancestor = arg), + "C" -> (_ => console = true), + "L:" -> (arg => log_file = Some(Path.explode(arg))), + "R:" -> (arg => { logic = arg; logic_requirements = true }), + "d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))), + "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), + "l:" -> (arg => logic = arg), + "m:" -> (arg => modes = modes ::: List(arg)), + "n" -> (_ => no_build = true), + "o:" -> add_option, + "p:" -> (arg => add_option("ML_process_policy=" + arg)), + "s" -> (_ => add_option("system_heaps=true")), + "u" -> (_ => add_option("system_heaps=false")), + "v" -> (_ => verbose = true)) val more_args = getopts(args) init_settings() - if (console) { - run_cli(more_args, progress = new Console_Progress()).check - } - else { - run_cli(List("--version")).check - run_cli(more_args, background = true).check - } + val (background, progress) = + if (console) (false, new Console_Progress) + else { run_cli(List("--version")).check; (true, new Progress) } + + run_cli(more_args, options = options, logic = logic, logic_ancestor = logic_ancestor, + logic_requirements = logic_requirements, session_dirs = session_dirs, + include_sessions = include_sessions, modes = modes, no_build = no_build, + log_file = log_file, verbose = verbose, background = background, progress = progress).check }) }