# HG changeset patch
# User wenzelm
# Date 881062743 -3600
# Node ID 4adf0b093275a424c0fcca59a88e04850e1a27dd
# Parent  f5d7fbb731038de1e8398ebcdf40329ce78f034a
added tmp_name;

diff -r f5d7fbb73103 -r 4adf0b093275 src/Pure/Thy/file.ML
--- a/src/Pure/Thy/file.ML	Tue Dec 02 12:38:39 1997 +0100
+++ b/src/Pure/Thy/file.ML	Tue Dec 02 12:39:03 1997 +0100
@@ -13,7 +13,9 @@
 signature FILE =
 sig
   include BASIC_FILE
+  val tmp_name: string -> string
   val exists: string -> bool
+  val info: string -> string
   val read: string -> string
   val write: string -> string -> unit
   val append: string -> string -> unit
@@ -24,9 +26,17 @@
 struct
 
 
-(* exists *)
+(* tmp_name *)
+
+fun tmp_name name =
+  Path.pack (Path.evaluate (Path.unpack o getenv)
+    (Path.append (Path.variable "ISABELLE_TMP") (Path.unpack name)));
+
+
+(* exists / info *)
 
 fun exists name = (file_info name <> "");
+val info = file_info;
 
 
 (* read / write files *)
@@ -52,7 +62,7 @@
     TextIO.closeOut outstream
   end;
 
-fun copy infile outfile =               (* FIXME improve *)
+fun copy infile outfile =
   if not (exists infile) then error ("File not found: " ^ quote infile)
   else write outfile (read infile);