# HG changeset patch
# User wenzelm
# Date 1646839274 -3600
# Node ID 41dfe941c3da6833ec21ac8742e0fccb2a4f60ad
# Parent  598b4a1f61dca204351c68e0f29b1ce434547ee3
inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs;

diff -r 598b4a1f61dc -r 41dfe941c3da lib/Tools/vscode
--- a/lib/Tools/vscode	Wed Mar 09 12:41:40 2022 +0100
+++ b/lib/Tools/vscode	Wed Mar 09 16:21:14 2022 +0100
@@ -4,8 +4,6 @@
 #
 # DESCRIPTION: run Isabelle/VSCode using local VSCodium installation
 
-export ISABELLE_VSCODE_SYMBOLS="$(platform_path "$ISABELLE_VSCODE_WORKSPACE/symbols.json")"
-
 DIR="$(isabelle vscode_setup -C)" || exit "$?"
 exec "$DIR/bin/codium" \
   --locale en-US \
diff -r 598b4a1f61dc -r 41dfe941c3da src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Wed Mar 09 12:41:40 2022 +0100
+++ b/src/Pure/General/json.scala	Wed Mar 09 16:21:14 2022 +0100
@@ -172,6 +172,8 @@
       try { Some(parse(s, strict = false)) }
       catch { case ERROR(_) => None }
 
+    def apply_lines(json: List[T]): S = json.map(apply).mkString("[", ",\n", "]")
+
     def apply(json: T): S =
     {
       val result = new StringBuilder
diff -r 598b4a1f61dc -r 41dfe941c3da src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Mar 09 12:41:40 2022 +0100
+++ b/src/Pure/General/symbol.scala	Wed Mar 09 16:21:14 2022 +0100
@@ -375,12 +375,12 @@
 
   object Symbols
   {
-    def load(): Symbols =
+    def load(static: Boolean = false): Symbols =
     {
-      val contents =
-        for (path <- Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS")) if path.is_file)
-          yield File.read(path)
-      make(cat_lines(contents))
+      val paths =
+        if (static) List(Path.explode("~~/etc/symbols"))
+        else Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS"))
+      make(cat_lines(for (path <- paths if path.is_file) yield File.read(path)))
     }
 
     def make(symbols_spec: String): Symbols =
diff -r 598b4a1f61dc -r 41dfe941c3da src/Tools/VSCode/etc/settings
--- a/src/Tools/VSCode/etc/settings	Wed Mar 09 12:41:40 2022 +0100
+++ b/src/Tools/VSCode/etc/settings	Wed Mar 09 16:21:14 2022 +0100
@@ -3,4 +3,3 @@
 ISABELLE_VSCODE_VERSION="1.65.0"
 ISABELLE_VSCODE_HOME="$ISABELLE_HOME/src/Tools/VSCode"
 ISABELLE_VSCODE_SETTINGS="$ISABELLE_HOME_USER/vscode"
-ISABELLE_VSCODE_WORKSPACE="$ISABELLE_VSCODE_SETTINGS/workspace"
diff -r 598b4a1f61dc -r 41dfe941c3da src/Tools/VSCode/extension/src/isabelle_encoding.ts
--- a/src/Tools/VSCode/extension/src/isabelle_encoding.ts	Wed Mar 09 12:41:40 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_encoding.ts	Wed Mar 09 16:21:14 2022 +0100
@@ -7,9 +7,6 @@
 
 import { TextEncoder, TextDecoder } from 'util'   // VSCODE: REMOVE
 
-const process = require('process');
-const fs = require('fs');
-
 
 /* defined symbols */
 
@@ -20,16 +17,13 @@
   abbrevs: string[];
 }
 
-const symbols_file = process.env['ISABELLE_VSCODE_SYMBOLS'];
-
-export const symbols: [Symbol_Entry] =
-  symbols_file ? JSON.parse(fs.readFileSync(symbols_file).toString()) : [];
+export const static_symbols: Symbol_Entry[] = [/*symbols*/];
 
 export const symbols_decode: Map<string, string> =
-  new Map(symbols.map((s: Symbol_Entry) => [s.symbol, String.fromCharCode(s.code)]));
+  new Map(static_symbols.map((s: Symbol_Entry) => [s.symbol, String.fromCharCode(s.code)]));
 
 export const symbols_encode: Map<string, string> =
-  new Map(symbols.map((s: Symbol_Entry) => [String.fromCharCode(s.code), s.symbol]));
+  new Map(static_symbols.map((s: Symbol_Entry) => [String.fromCharCode(s.code), s.symbol]));
 
 
 /* encoding */
diff -r 598b4a1f61dc -r 41dfe941c3da src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Wed Mar 09 12:41:40 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Wed Mar 09 16:21:14 2022 +0100
@@ -10,6 +10,7 @@
 'use strict';
 
 import * as file from './file'
+import * as library from './library'
 import * as isabelle_encoding from './isabelle_encoding'
 
 
@@ -49,10 +50,10 @@
 
 export class Symbols
 {
-  entries: [Entry]
+  entries: Entry[]
   private entries_map: Map<Symbol, Entry>
 
-  constructor(entries: [Entry])
+  constructor(entries: Entry[])
   {
     this.entries = entries
     this.entries_map = new Map<Symbol, Entry>()
@@ -72,4 +73,14 @@
   }
 }
 
-export const symbols: Symbols = new Symbols(isabelle_encoding.symbols)
+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"
+    return file.read_json_sync(file.platform_path(path))
+  }
+  else { return [] }
+}
+
+export const symbols: Symbols = new Symbols(load_symbols())
diff -r 598b4a1f61dc -r 41dfe941c3da src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Wed Mar 09 12:41:40 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Wed Mar 09 16:21:14 2022 +0100
@@ -26,6 +26,25 @@
   def vscodium_exe(dir: Path): Path = dir + Path.explode("bin/codium")
 
 
+  /* Isabelle symbols (static subset) */
+
+  val symbols_json: Path = Path.explode("symbols.json")
+
+  def write_symbols(dir: Path, json: List[JSON.T]): Unit =
+    File.write(Isabelle_System.make_directory(dir) + symbols_json, JSON.Format.apply_lines(json))
+
+  def load_symbols_static(): List[JSON.T] =
+  {
+    val symbols = Symbol.Symbols.load(static = true)
+    for (entry <- symbols.entries; code <- entry.code)
+      yield JSON.Object(
+        "symbol" -> entry.symbol,
+        "name" -> entry.name,
+        "code" -> code,
+        "abbrevs" -> entry.abbrevs)
+  }
+
+
   /* platform info */
 
   sealed case class Platform_Info(
@@ -86,14 +105,6 @@
       (("MS_TAG=" + Bash.string(version)) :: "SHOULD_BUILD=yes" :: "VSCODE_ARCH=x64" :: env)
         .map(s => "export " + s + "\n").mkString
 
-    def resources_dir(dir: Path): Path =
-    {
-      val resources =
-        if (platform == Platform.Family.macos) "VSCodium.app/Contents/Resources"
-        else "resources"
-      dir + Path.explode(resources)
-    }
-
     def patch_sources(base_dir: Path): String =
     {
       val dir = base_dir + Path.explode("vscode")
@@ -112,12 +123,16 @@
             Path.explode("$ISABELLE_VSCODE_HOME/extension/src/isabelle_encoding.ts")
           val common_dir = dir + Path.explode("src/vs/workbench/services/textfile/common")
 
+          val inline_symbols = JSON.Format.apply_lines(load_symbols_static())
+
           val header =
             split_lines(File.read(common_dir + Path.explode("encoding.ts")))
               .takeWhile(_.trim.nonEmpty)
           val body =
-            split_lines(File.read(isabelle_encodings))
-              .filterNot(_.containsSlice("// VSCODE: REMOVE"))
+            for {
+              line <- split_lines(File.read(isabelle_encodings))
+              if !line.containsSlice("// VSCODE: REMOVE")
+            } yield line.replace("[/*symbols*/]", inline_symbols)
 
           File.write(common_dir + isabelle_encodings.base, cat_lines(header ::: body))
         }
@@ -137,9 +152,14 @@
 
     def patch_resources(base_dir: Path): String =
     {
-      val dir = resources_dir(base_dir)
+      val dir = base_dir + Path.explode("resources")
+      if (platform == Platform.Family.macos) {
+        Isabelle_System.symlink(base_dir + Path.explode("VSCodium.app/Contents/Resources"), dir)
+      }
       Isabelle_System.with_copy_dir(dir, dir.orig) {
-        HTML.init_fonts(dir + Path.explode("app/out/vs/base/browser/ui"))
+        val fonts_dir = dir + Path.explode("app/out/vs/base/browser/ui/fonts")
+        HTML.init_fonts(fonts_dir.dir)
+        write_symbols(fonts_dir, load_symbols_static())
 
         val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css")
         val checksum1 = file_checksum(workbench_css)
@@ -163,10 +183,12 @@
       Isabelle_System.with_tmp_dir("download")(download_dir =>
       {
         download(download_dir, progress = progress)
-        for (name <- Seq("app/node_modules.asar", "app/node_modules.asar.unpacked")) {
-          val rel_path = resources_dir(Path.current) + Path.explode(name)
-          Isabelle_System.rm_tree(dir + rel_path)
-          Isabelle_System.copy_dir(download_dir + rel_path, dir + rel_path)
+        for {
+          name <- Seq("resources/app/node_modules.asar", "resources/app/node_modules.asar.unpacked")
+        } {
+          val path = Path.explode(name)
+          Isabelle_System.rm_tree(dir + path)
+          Isabelle_System.copy_dir(download_dir + path, dir + path)
         }
       })
     }
@@ -194,6 +216,7 @@
     }
   }
 
+
   // see https://github.com/microsoft/vscode/blob/main/build/gulpfile.vscode.js
   // function computeChecksum(filename)
   private def file_checksum(path: Path): String =
diff -r 598b4a1f61dc -r 41dfe941c3da src/Tools/VSCode/src/vscode_setup.scala
--- a/src/Tools/VSCode/src/vscode_setup.scala	Wed Mar 09 12:41:40 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Wed Mar 09 16:21:14 2022 +0100
@@ -20,7 +20,6 @@
   def vscode_home: Path = Path.variable("ISABELLE_VSCODE_HOME")
   def vscode_settings: Path = Path.variable("ISABELLE_VSCODE_SETTINGS")
   def vscode_settings_user: Path = vscode_settings + Path.explode("user-data/User/settings.json")
-  def vscode_workspace: Path = Path.variable("ISABELLE_VSCODE_WORKSPACE")
   def version: String = Build_VSCodium.version
 
   def vscodium_home: Path = Path.variable("ISABELLE_VSCODIUM_HOME")
@@ -69,27 +68,6 @@
   }
 
 
-  /* workspace */
-
-  def init_workspace(dir: Path): Unit =
-  {
-    Isabelle_System.make_directory(dir)
-    Isabelle_System.chmod("700", dir)
-
-    File.change(dir + Path.explode("symbols.json"), init = true) { _ =>
-      JSON.Format(
-        for (entry <- Symbol.symbols.entries; code <- entry.code)
-          yield JSON.Object(
-            "symbol" -> entry.symbol,
-            "name" -> entry.name,
-            "code" -> code,
-            "abbrevs" -> entry.abbrevs
-          )
-      )
-    }
-  }
-
-
   /* vscode setup */
 
   def default_platform: Platform.Family.Value = Platform.family
@@ -125,11 +103,9 @@
 
     if (check) {
       if (vscodium_home_ok()) {
-        init_workspace(vscode_workspace)
         progress.echo(vscodium_home.expand.implode)
       }
       else if (install_ok) {
-        init_workspace(vscode_workspace)
         progress.echo(install_dir.expand.implode)
       }
       else {