# HG changeset patch
# User wenzelm
# Date 1670764232 -3600
# Node ID 7af197063e2f57ce53942655ea64f98f9f0b7d97
# Parent  fb322b989584401e2e73e53785b897f3e88b14b6
clarified signature: copy directory content more directly;

diff -r fb322b989584 -r 7af197063e2f src/Pure/Admin/build_prismjs.scala
--- a/src/Pure/Admin/build_prismjs.scala	Sun Dec 11 14:05:12 2022 +0100
+++ b/src/Pure/Admin/build_prismjs.scala	Sun Dec 11 14:10:32 2022 +0100
@@ -36,11 +36,8 @@
     Isabelle_System.with_tmp_dir("tmp") { tmp_dir =>
       Isabelle_System.bash("npm init -y && npm install prismjs@" + Bash.string(version),
         cwd = tmp_dir.file).check
-
-      Isabelle_System.rm_tree(component_dir.path)
       Isabelle_System.copy_dir(tmp_dir + Path.explode("node_modules/prismjs"),
-        component_dir.path)
-      Isabelle_System.make_directory(component_dir.etc)
+        component_dir.path, direct = true)
     }
 
 
diff -r fb322b989584 -r 7af197063e2f src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Dec 11 14:05:12 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Dec 11 14:10:32 2022 +0100
@@ -162,12 +162,14 @@
     if (path.is_dir) error("Directory already exists: " + path.absolute)
     else make_directory(path)
 
-  def copy_dir(dir1: Path, dir2: Path): Unit = {
+  def copy_dir(dir1: Path, dir2: Path, direct: Boolean = false): Unit = {
     def make_path(dir: Path): String = {
-      File.standard_path(dir.absolute)
+      val s = File.standard_path(dir.absolute)
+      if (direct) Url.direct_path(s) else s
     }
     val p1 = make_path(dir1)
     val p2 = make_path(dir2)
+    if (direct) make_directory(dir2)
     val res = bash("cp -a " + Bash.string(p1) + " " + Bash.string(p2))
     if (!res.ok) cat_error("Failed to copy " + quote(p1) + " to " + quote(p2), res.err)
   }
@@ -188,7 +190,7 @@
 
   object Copy_Dir extends Scala.Fun_Strings("copy_dir") {
     val here = Scala_Project.here
-    def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir)
+    def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir(_, _))
   }