src/Pure/library.ML

 Basic library: functions, options, pairs, booleans, lists, integers,
 strings, lists as sets, association lists, generic tables, balanced trees,
 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 =
 struct
 

 
 (*For Makefiles: use the file, but exit with error code if errors found.*)
 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"*)
 val split_filename =
   (pairself implode) o take_suffix (not_equal "/") o explode;

      else ();
      space_implode "/" (mk_relative (space_explode "/" cur_path)
                                     (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 **)
 
 (*use the keyfun to make a list of (x, key) pairs*)
 fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =