fail_safe close;
added sys_unpack hook;
added pwd;
removed join_info;

--- a/src/Pure/General/file.ML	Thu Feb 04 18:13:10 1999 +0100
+++ b/src/Pure/General/file.ML	Thu Feb 04 18:14:27 1999 +0100
@@ -3,36 +3,52 @@
     Author:     Markus Wenzel, TU Muenchen
 
 File system operations.
-
-TODO:
-  - close in case of error (!?);
 *)
 
 signature FILE =
 sig
-  val sys_path_fn: (Path.T -> string) ref
+  val sys_pack_fn: (Path.T -> string) ref
+  val sys_unpack_fn: (string -> Path.T) ref
+  val use: Path.T -> unit
+  val rm: Path.T -> unit
+  val cd: Path.T -> unit
+  val pwd: unit -> Path.T
+  val full_path: Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
-  eqtype info
-  val info: Path.T -> info option
-  val join_info: info -> info -> info
-  val exists: Path.T -> bool
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
   val copy: Path.T -> Path.T -> unit
-  val use: Path.T -> unit
-  val cd: Path.T -> unit
-  val rm: Path.T -> unit
+  eqtype info
+  val info: Path.T -> info option
+  val exists: Path.T -> bool
 end;
 
 structure File: FILE =
 struct
 
 
-(* sys_path (default for Unix) *)
+(* system path representations (default: Unix) *)
+
+val sys_pack_fn = ref Path.pack;
+val sys_unpack_fn = ref Path.unpack;
+
+fun sysify path = ! sys_pack_fn (Path.expand path);
+fun unsysify s = ! sys_unpack_fn s;
+
 
-val sys_path_fn = ref Path.pack;
-fun sysify path = ! sys_path_fn (Path.expand path);
+val use = use o sysify;
+val rm = OS.FileSys.remove o sysify;
+
+
+(* current path *)
+
+val cd = Library.cd o sysify;
+val pwd = unsysify o Library.pwd;
+
+fun full_path path =
+  if Path.is_absolute path then path
+  else Path.append (pwd ()) path;
 
 
 (* tmp_path *)
@@ -41,53 +57,34 @@
   Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
 
 
-(* info / exists *)
+(* read / write files *)
+
+fun fail_safe f g x =
+  let val y = f x handle exn => (g x; raise exn)
+  in g x; y end;
+
+
+fun output txt stream = TextIO.output (stream, txt);
 
-datatype info = Info of string list;
+fun read path = fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (sysify path));
+fun write path txt = fail_safe (output txt) TextIO.closeOut (TextIO.openOut (sysify path));
+fun append path txt = fail_safe (output txt) TextIO.closeOut (TextIO.openAppend (sysify path));
 
-fun join_info (Info xs) (Info ys) = Info (xs @ ys);
+fun copy inpath outpath = write outpath (read inpath);
+
+
+(* file info *)
+
+datatype info = Info of string;
 
 fun info path =
   let val name = sysify path in
     (case file_info name of
       "" => None
-    | s => Some (Info [name ^ ": " ^ s]))	(* FIXME include full path (!?) *)
+    | s => Some (Info s))
   end;
 
 val exists = is_some o info;
 
 
-(* read / write files *)
-
-fun read path =
-  let
-    val instream  = TextIO.openIn (sysify path);
-    val intext = TextIO.inputAll instream;
-  in
-    TextIO.closeIn instream;
-    intext
-  end;
-
-fun write path txt =
-  let val outstream = TextIO.openOut (sysify path) in
-    TextIO.output (outstream, txt);
-    TextIO.closeOut outstream
-  end;
-
-fun append path txt =
-  let val outstream = TextIO.openAppend (sysify path) in
-    TextIO.output (outstream, txt);
-    TextIO.closeOut outstream
-  end;
-
-fun copy inpath outpath = write outpath (read inpath);
-
-
-(* misc operations *)
-
-val use = use o sysify;
-val cd = Library.cd o sysify;
-val rm = OS.FileSys.remove o sysify;
-
-
 end;