# HG changeset patch
# User wenzelm
# Date 1129032152 -7200
# Node ID afa2696eacce989c1994a98b8c5169e31d8d3319
# Parent  ede984daba01b4fff133ae7476dbb0dbd90b4d07
added assert;
tuned;

diff -r ede984daba01 -r afa2696eacce src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Tue Oct 11 13:30:17 2005 +0200
+++ b/src/Pure/General/file.ML	Tue Oct 11 14:02:32 2005 +0200
@@ -19,6 +19,12 @@
   val tmp_path: Path.T -> Path.T
   val isatool: string -> int
   val system_command: string -> unit
+  eqtype info
+  val info: Path.T -> info option
+  val exists: Path.T -> bool
+  val assert: Path.T -> unit
+  val rm: Path.T -> unit
+  val mkdir: Path.T -> unit
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
@@ -27,11 +33,6 @@
   val eq: Path.T * Path.T -> bool
   val copy: Path.T -> Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
-  eqtype info
-  val info: Path.T -> info option
-  val exists: Path.T -> bool
-  val rm: Path.T -> unit
-  val mkdir: Path.T -> unit
   val use: Path.T -> unit
 end;
 
@@ -93,6 +94,10 @@
 
 val exists = is_some o info;
 
+fun assert path =
+  if exists path then ()
+  else error ("No such file or directory: " ^ quote (Path.pack path));
+
 val rm = OS.FileSys.remove o platform_path;
 
 fun mkdir path = system_command ("mkdir -p " ^ shell_path path);