# HG changeset patch
# User wenzelm
# Date 1647291437 -3600
# Node ID b9dde91f9106c3bc2374aced8faf3d8aef43d2a7
# Parent  686a6d7d09915fa34e83cb81d5148aeb573e8a9d# Parent  9229f2681db78033bdadddba94558d9c51bfea28
merged

diff -r 686a6d7d0991 -r b9dde91f9106 lib/Tools/electron
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/electron	Mon Mar 14 21:57:17 2022 +0100
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: run the Electron framework (with its own command-line arguments)
+
+exec "$ISABELLE_VSCODIUM_ELECTRON" "$@"
diff -r 686a6d7d0991 -r b9dde91f9106 lib/Tools/vscode
--- a/lib/Tools/vscode	Fri Mar 11 11:19:38 2022 +0100
+++ b/lib/Tools/vscode	Mon Mar 14 21:57:17 2022 +0100
@@ -6,8 +6,11 @@
 
 isabelle vscode_setup || exit "$?"
 
-exec "$ISABELLE_VSCODIUM_HOME/vscodium" \
-  --locale en-US \
+export ISABELLE_VSCODIUM_APP="$(platform_path "$ISABELLE_VSCODIUM_RESOURCES/vscodium")"
+
+ELECTRON_RUN_AS_NODE=1 "$ISABELLE_VSCODIUM_ELECTRON" \
+  "$(platform_path "$ISABELLE_VSCODIUM_RESOURCES/vscodium/out/cli.js")" \
+  --ms-enable-electron-run-as-node --locale en-US \
   --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \
   --extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \
   "$@"
diff -r 686a6d7d0991 -r b9dde91f9106 src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Fri Mar 11 11:19:38 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Mon Mar 14 21:57:17 2022 +0100
@@ -79,9 +79,9 @@
 
 function load_symbols(): Entry[]
 {
-  const vscodium_home = library.getenv("ISABELLE_VSCODIUM_HOME")
-  if (vscodium_home) {
-    const path = vscodium_home + "/resources/app/out/vs/base/browser/ui/fonts/symbols.json"
+  const vscodium_resources = library.getenv("ISABELLE_VSCODIUM_RESOURCES")
+  if (vscodium_resources) {
+    const path = vscodium_resources + "/vscodium/out/vs/base/browser/ui/fonts/symbols.json"
     return file.read_json_sync(file.platform_path(path))
   }
   else { return [] }
diff -r 686a6d7d0991 -r b9dde91f9106 src/Tools/VSCode/patches/cli.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/patches/cli.patch	Mon Mar 14 21:57:17 2022 +0100
@@ -0,0 +1,25 @@
+diff --git a/src/vs/code/node/cli.ts b/src/vs/code/node/cli.ts
+--- a/src/vs/code/node/cli.ts
++++ b/src/vs/code/node/cli.ts
+@@ -363,9 +363,11 @@ export async function main(argv: string[]): Promise<any> {
+ 		}
+ 
+ 		let child: ChildProcess;
++		const app_arg = '--app=' + process.env['ISABELLE_VSCODIUM_APP'];
++		const electron_args = [app_arg].concat(argv.slice(2));
+ 		if (!isMacOSBigSurOrNewer) {
+ 			// We spawn process.execPath directly
+-			child = spawn(process.execPath, argv.slice(2), options);
++			child = spawn(process.execPath, electron_args, options);
+ 		} else {
+ 			// On Big Sur, we spawn using the open command to obtain behavior
+ 			// similar to if the app was launched from the dock
+@@ -425,7 +427,7 @@ export async function main(argv: string[]): Promise<any> {
+ 				}
+ 			}
+ 
+-			spawnArgs.push('--args', ...argv.slice(2)); // pass on our arguments
++			spawnArgs.push('--args', ...electron_args); // pass on our arguments
+ 
+ 			if (env['VSCODE_DEV']) {
+ 				// If we're in development mode, replace the . arg with the
diff -r 686a6d7d0991 -r b9dde91f9106 src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Fri Mar 11 11:19:38 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Mon Mar 14 21:57:17 2022 +0100
@@ -22,6 +22,8 @@
   val vscodium_repository = "https://github.com/VSCodium/vscodium.git"
   val vscodium_download = "https://github.com/VSCodium/vscodium/releases/download"
 
+  private val resources = Path.explode("resources")
+
 
   /* Isabelle symbols (static subset only) */
 
@@ -140,7 +142,7 @@
         // explicit patches
         {
           val patches_dir = Path.explode("$ISABELLE_VSCODE_HOME/patches")
-          for (name <- Seq("isabelle_encoding", "no_ocaml_icons")) {
+          for (name <- Seq("cli", "isabelle_encoding", "no_ocaml_icons")) {
             val path = patches_dir + Path.explode(name).patch
             Isabelle_System.bash("patch -p1 < " + File.bash_path(path), cwd = dir.file).check
           }
@@ -152,36 +154,48 @@
 
     def patch_resources(base_dir: Path): String =
     {
-      val dir = base_dir + Path.explode("resources")
-      Isabelle_System.with_copy_dir(dir, dir.orig) {
-        val fonts_dir = dir + Path.explode("app/out/vs/base/browser/ui/fonts")
-        HTML.init_fonts(fonts_dir.dir)
-        make_symbols().write(fonts_dir)
+      val dir = base_dir + resources
+      val patch =
+        Isabelle_System.with_copy_dir(dir, dir.orig) {
+          val fonts_dir = dir + Path.explode("app/out/vs/base/browser/ui/fonts")
+          HTML.init_fonts(fonts_dir.dir)
+          make_symbols().write(fonts_dir)
 
-        val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css")
-        val checksum1 = file_checksum(workbench_css)
-        File.append(workbench_css, "\n\n" + HTML.fonts_css_dir(prefix = "../base/browser/ui"))
-        val checksum2 = file_checksum(workbench_css)
+          val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css")
+          val checksum1 = file_checksum(workbench_css)
+          File.append(workbench_css, "\n\n" + HTML.fonts_css_dir(prefix = "../base/browser/ui"))
+          val checksum2 = file_checksum(workbench_css)
 
-        val file_name = workbench_css.file_name
-        File.change_lines(dir + Path.explode("app/product.json")) { _.map(line =>
-          if (line.containsSlice(file_name) && line.contains(checksum1)) {
-            line.replace(checksum1, checksum2)
+          val file_name = workbench_css.file_name
+          File.change_lines(dir + Path.explode("app/product.json")) { _.map(line =>
+            if (line.containsSlice(file_name) && line.contains(checksum1)) {
+              line.replace(checksum1, checksum2)
+            }
+            else line)
           }
-          else line)
+
+          Isabelle_System.make_patch(dir.dir, dir.orig.base, dir.base)
         }
 
-        Isabelle_System.make_patch(dir.dir, dir.orig.base, dir.base)
+      val app_dir = dir + Path.explode("app")
+      val vscodium_app_dir = dir + Path.explode("vscodium")
+      Isabelle_System.move_file(app_dir, vscodium_app_dir)
+
+      Isabelle_System.make_directory(app_dir)
+      if ((vscodium_app_dir + resources).is_dir) {
+        Isabelle_System.copy_dir(vscodium_app_dir + resources, app_dir)
       }
+
+      patch
     }
 
     def init_resources(base_dir: Path): Path =
     {
-      val resources_dir = base_dir + Path.explode("resources")
+      val dir = base_dir + resources
       if (platform == Platform.Family.macos) {
-        Isabelle_System.symlink(Path.explode("VSCodium.app/Contents/Resources"), resources_dir)
+        Isabelle_System.symlink(Path.explode("VSCodium.app/Contents/Resources"), dir)
       }
-      resources_dir
+      dir
     }
 
     def setup_node(target_dir: Path, progress: Progress): Unit =
@@ -205,13 +219,12 @@
       platform match {
         case Platform.Family.linux | Platform.Family.linux_arm =>
           Isabelle_System.move_file(dir + Path.explode("codium"), dir + electron)
-        case Platform.Family.macos =>
-          Isabelle_System.symlink(Path.explode("VSCodium.app/Contents/MacOS/Electron"), dir + electron)
         case Platform.Family.windows =>
           Isabelle_System.move_file(dir + Path.explode("VSCodium.exe"), dir + electron.exe)
           Isabelle_System.move_file(
             dir + Path.explode("VSCodium.VisualElementsManifest.xml"),
             dir + Path.explode("electron.VisualElementsManifest.xml"))
+        case Platform.Family.macos =>
       }
     }
 
@@ -219,16 +232,6 @@
     {
       Isabelle_System.rm_tree(dir + Path.explode("bin"))
 
-      val exe = dir + Path.explode("vscodium")
-      File.write(exe, """#!/usr/bin/env bash
-
-unset CDPATH
-THIS="$(cd "$(dirname "$0")"; pwd -P)"
-
-ELECTRON_RUN_AS_NODE=1 "$THIS/electron" "$THIS/resources/app/out/cli.js" --ms-enable-electron-run-as-node "$@"
-""")
-      File.set_executable(exe, true)
-
       if (platform == Platform.Family.windows) {
         val files =
           File.find_files(dir.file, pred = file =>
@@ -388,6 +391,10 @@
         val resources_patch = platform_info.patch_resources(platform_dir)
         if (platform_info.is_linux) write_patch("03-isabelle_resources", resources_patch)
 
+        Isabelle_System.copy_file(
+          build_dir + Path.explode("vscode/node_modules/electron/dist/resources/default_app.asar"),
+          platform_dir + resources)
+
         platform_info.setup_executables(platform_dir)
       })
     }
@@ -402,6 +409,14 @@
       """# -*- shell-script -*- :mode=shellscript:
 
 ISABELLE_VSCODIUM_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
+
+if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then
+  ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/MacOS/Electron"
+  ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/Resources"
+else
+  ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/electron"
+  ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/resources"
+fi
 """)