added subdir_of
authorclasohm
Mon Dec 18 12:28:00 1995 +0100 (1995-12-18)
changeset 1407c22cc592785f
parent 1406 dc73ca67b5ac
child 1408 fcb3346c9922
added subdir_of
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Dec 15 12:23:56 1995 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Dec 18 12:28:00 1995 +0100
     1.3 @@ -8,7 +8,8 @@
     1.4  input / output, timing, filenames, misc functions.
     1.5  *)
     1.6  
     1.7 -infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset;
     1.8 +infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset
     1.9 +      subdir_of;
    1.10  
    1.11  
    1.12  structure Library =
    1.13 @@ -695,7 +696,7 @@
    1.14  fun exit_use fname = use fname handle _ => exit 1;
    1.15  
    1.16  
    1.17 -(** filenames **)
    1.18 +(** filenames and paths **)
    1.19  
    1.20  (*Convert UNIX filename of the form "path/file" to "path/" and "file";
    1.21    if filename contains no slash, then it returns "" and "file"*)
    1.22 @@ -731,6 +732,12 @@
    1.23                                      (space_explode "/" dest_path))
    1.24    end;
    1.25  
    1.26 +(*Determine if absolute path1 is a subdirectory of absolute path2*)
    1.27 +fun path1 subdir_of path2 =
    1.28 +  if hd (explode path1) <> "/" orelse hd (explode path2) <> "/" then
    1.29 +    error "Relative or empty path passed to subdir_of"
    1.30 +  else (space_explode "/" path2) prefix (space_explode "/" path1);
    1.31 +
    1.32  
    1.33  (** misc functions **)
    1.34