command-line arguments for "isabelle vscode", similar to "isabelle jedit";

--- 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)
 }

--- 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)
 

--- 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",

--- 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<Array<string>>("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: [

--- 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!"
 

--- 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
     })
 }