# HG changeset patch
# User clasohm
# Date 819286080 -3600
# Node ID c22cc592785ffd822d55144b091a3f6e74cd2048
# Parent  dc73ca67b5acd9b1934e5a3d9bfa907949b9574f
added subdir_of

diff -r dc73ca67b5ac -r c22cc592785f src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Dec 15 12:23:56 1995 +0100
+++ b/src/Pure/library.ML	Mon Dec 18 12:28:00 1995 +0100
@@ -8,7 +8,8 @@
 input / output, timing, filenames, misc functions.
 *)
 
-infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset;
+infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset
+      subdir_of;
 
 
 structure Library =
@@ -695,7 +696,7 @@
 fun exit_use fname = use fname handle _ => exit 1;
 
 
-(** filenames **)
+(** filenames and paths **)
 
 (*Convert UNIX filename of the form "path/file" to "path/" and "file";
   if filename contains no slash, then it returns "" and "file"*)
@@ -731,6 +732,12 @@
                                     (space_explode "/" dest_path))
   end;
 
+(*Determine if absolute path1 is a subdirectory of absolute path2*)
+fun path1 subdir_of path2 =
+  if hd (explode path1) <> "/" orelse hd (explode path2) <> "/" then
+    error "Relative or empty path passed to subdir_of"
+  else (space_explode "/" path2) prefix (space_explode "/" path1);
+
 
 (** misc functions **)