# HG changeset patch
# User wenzelm
# Date 1648151114 -3600
# Node ID 96a33aaf23a1e36b8165d09f4fb0b3aa02c1c14a
# Parent  8fcf5770863633951f662de545f2ac901764e783
clarified options;
tuned messages;

diff -r 8fcf57708636 -r 96a33aaf23a1 src/Tools/VSCode/src/build_vscode_extension.scala
--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Wed Mar 23 20:26:33 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Thu Mar 24 20:45:14 2022 +0100
@@ -172,21 +172,18 @@
       var dirs: List[Path] = Nil
       var logic = default_logic
       var install = false
-      var uninstall = false
 
       val getopts = Getopts("""
 Usage: isabelle build_vscode_extension
 
   Options are:
     -I           install resulting extension
-    -U           uninstall extension (no build)
     -d DIR       include session directory
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
 
 Build Isabelle/VSCode extension module (vsix).
 """,
         "I" -> (_ => install = true),
-        "U" -> (_ => uninstall = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "l:" -> (arg => logic = arg))
 
@@ -196,11 +193,8 @@
       val options = Options.init()
       val progress = new Console_Progress()
 
-      if (uninstall) VSCode_Main.uninstall_extension(progress = progress)
-      else {
-        val vsix = build_extension(options, logic = logic, dirs = dirs, progress = progress)
-        vsix.write(VSCode_Main.extension_dir)
-        if (install) VSCode_Main.install_extension(vsix, progress = progress)
-      }
+      val vsix = build_extension(options, logic = logic, dirs = dirs, progress = progress)
+      vsix.write(VSCode_Main.extension_dir)
+      if (install) VSCode_Main.install_extension(vsix, progress = progress)
     })
 }
diff -r 8fcf57708636 -r 96a33aaf23a1 src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Wed Mar 23 20:26:33 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Thu Mar 24 20:45:14 2022 +0100
@@ -133,11 +133,10 @@
 
   def uninstall_extension(progress: Progress = new Progress): Unit =
     locate_extension() match {
-      case None => progress.echo_warning("No extension " + quote(extension_name) + " to uninstall")
+      case None => progress.echo_warning("No Isabelle/VSCode extension to uninstall")
       case Some(dir) =>
         run_vscodium(List("--uninstall-extension", extension_name)).check
-        progress.echo("Uninstalled extension " + quote(extension_name) +
-          " from directory:\n  " + dir)
+        progress.echo("Uninstalled Isabelle/VSCode extension from directory:\n  " + dir)
     }
 
   def install_extension(vsix: File.Content, progress: Progress = new Progress): Unit =
@@ -147,10 +146,9 @@
       vsix.write(tmp_dir)
       run_vscodium(List("--install-extension", File.platform_path(tmp_dir + vsix.path))).check
       locate_extension() match {
-        case None => error("No extension " + extension_name + " after installation")
+        case None => error("Missing extension Isabelle/VSCode after installation")
         case Some(dir) =>
-          progress.echo("Installed extension " + quote(extension_name) +
-            " into directory:\n  " + dir)
+          progress.echo("Installed Isabelle/VSCode extension into directory:\n  " + dir)
       }
     })
   }
@@ -191,8 +189,10 @@
     {
       var logic_ancestor = ""
       var console = false
+      var edit_extension = true
       var server_log = false
       var logic_requirements = false
+      var uninstall = false
       var session_dirs = List.empty[Path]
       var include_sessions = List.empty[String]
       var logic = ""
@@ -208,9 +208,11 @@
 
     -A NAME      ancestor session for option -R (default: parent)
     -C           run as foreground process, with console output
+    -E           edit Isabelle/VSCode extension project sources
     -L           enable language server log to file:
                  """ + server_log_path.implode + """
     -R NAME      build image with requirements from other sessions
+    -U           uninstall Isabelle/VSCode extension
     -d DIR       include session directory
     -i NAME      include session in name-space of theories
     -l NAME      logic session name
@@ -229,8 +231,10 @@
 """ + default_settings,
         "A:" -> (arg => logic_ancestor = arg),
         "C" -> (_ => console = true),
+        "E" -> (_ => edit_extension = true),
         "L" -> (_ => server_log = true),
         "R:" -> (arg => { logic = arg; logic_requirements = true }),
+        "U" -> (_ => uninstall = true),
         "d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))),
         "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
         "l:" -> (arg => { logic = arg; logic_requirements = false }),
@@ -246,14 +250,20 @@
 
       init_settings()
 
-      val (background, progress) =
-        if (console) (false, new Console_Progress)
+      val console_progress = new Console_Progress
+
+      if (uninstall) uninstall_extension(progress = console_progress)
+
+      val (background, app_progress) =
+        if (console) (false, console_progress)
         else { run_vscodium(List("--version")).check; (true, new Progress) }
 
-      run_vscodium(more_args, options = options, logic = logic, logic_ancestor = logic_ancestor,
+      run_vscodium(
+        more_args ::: (if (edit_extension) List(File.platform_path(extension_dir)) else Nil),
+        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,
         server_log = server_log, verbose = verbose, background = background,
-        progress = progress).check
+        progress = app_progress).check
     })
 }