# HG changeset patch
# User wenzelm
# Date 1605124525 -3600
# Node ID e7e93c0f6d962172e08eb190e392f49e096836f4
# Parent  ab4a0b19648adeb7ae6b9fe503b74f08a19e82d6
more operations (as in Isabelle/ML);

diff -r ab4a0b19648a -r e7e93c0f6d96 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Nov 10 12:48:56 2020 +0100
+++ b/src/Pure/General/file.scala	Wed Nov 11 20:55:25 2020 +0100
@@ -323,6 +323,14 @@
 
   def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
 
+  def copy_base(base_dir: Path, src0: Path, target_dir: Path)
+  {
+    val src = src0.expand
+    val src_dir = src.dir
+    if (!src.starts_basic) error("Illegal path specification " + src + " beyond base directory")
+    copy(base_dir + src, Isabelle_System.make_directory(target_dir + src_dir))
+  }
+
 
   /* move */
 
diff -r ab4a0b19648a -r e7e93c0f6d96 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Nov 10 12:48:56 2020 +0100
+++ b/src/Pure/General/path.scala	Wed Nov 11 20:55:25 2020 +0100
@@ -156,6 +156,7 @@
   def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
   def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
   def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
+  def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic]
 
   def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))