# HG changeset patch
# User wenzelm
# Date 1647976001 -3600
# Node ID e8c1d982b2752f8c8e119ded42e5302291139fbc
# Parent  171ac44913cac78b7fd6c374053c04a9e9b60597
tuned signature;

diff -r 171ac44913ca -r e8c1d982b275 src/Tools/VSCode/src/build_vscode_extension.scala
--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Tue Mar 22 19:33:38 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Tue Mar 22 20:06:41 2022 +0100
@@ -137,7 +137,11 @@
 
   /* extension */
 
-  lazy val extension_dir = Path.explode("$ISABELLE_VSCODE_HOME/extension")
+  def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension")
+  def extension_manifest: Path = extension_dir + Path.explode("MANIFEST")
+  def manifest_entries(): List[Path] =
+    for (line <- split_lines(File.read(extension_manifest)) if line.nonEmpty)
+      yield Path.explode(line)
 
   def build_extension(options: Options,
     logic: String = default_logic,
@@ -150,11 +154,7 @@
 
     Isabelle_System.with_tmp_dir("build")(build_dir =>
     {
-      for {
-        line <- split_lines(File.read(extension_dir + Path.explode("MANIFEST")))
-        if line.nonEmpty
-      } {
-        val path = Path.explode(line)
+      for (path <- manifest_entries()) {
         Isabelle_System.copy_file(extension_dir + path,
           Isabelle_System.make_directory(build_dir + path.dir))
       }