# HG changeset patch
# User wenzelm
# Date 897472220 -7200
# Node ID 05b152a419223478b84eced62e5a884d32069d19
# Parent  6f56d9650ee93c158cc61029376fd464611230ab
moved Thy/file.ML to General/file.ML;

diff -r 6f56d9650ee9 -r 05b152a41922 src/Pure/General/file.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/file.ML	Wed Jun 10 11:50:20 1998 +0200
@@ -0,0 +1,64 @@
+(*  Title:      Pure/Thy/file.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+File system operations.
+*)
+
+signature FILE =
+sig
+  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
+  val copy: string -> string -> unit
+end;
+
+structure File: FILE =
+struct
+
+
+(* 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 *)
+
+fun read name =
+  let
+    val instream  = TextIO.openIn name;
+    val intext = TextIO.inputAll instream;
+  in
+    TextIO.closeIn instream;
+    intext
+  end;
+
+fun write name txt =
+  let val outstream = TextIO.openOut name in
+    TextIO.output (outstream, txt);
+    TextIO.closeOut outstream
+  end;
+
+fun append name txt =
+  let val outstream = TextIO.openAppend name in
+    TextIO.output (outstream, txt);
+    TextIO.closeOut outstream
+  end;
+
+fun copy infile outfile =
+  if not (exists infile) then error ("File not found: " ^ quote infile)
+  else write outfile (read infile);
+
+
+end;
diff -r 6f56d9650ee9 -r 05b152a41922 src/Pure/Thy/file.ML
--- a/src/Pure/Thy/file.ML	Wed Jun 10 11:49:41 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(*  Title:      Pure/Thy/file.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-File system operations.
-*)
-
-signature FILE =
-sig
-  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
-  val copy: string -> string -> unit
-  val source: string -> (string, string list) Source.source
-end;
-
-structure File: FILE =
-struct
-
-
-(* 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 *)
-
-fun read name =
-  let
-    val instream  = TextIO.openIn name;
-    val intext = TextIO.inputAll instream;
-  in
-    TextIO.closeIn instream;
-    intext
-  end;
-
-fun write name txt =
-  let val outstream = TextIO.openOut name in
-    TextIO.output (outstream, txt);
-    TextIO.closeOut outstream
-  end;
-
-fun append name txt =
-  let val outstream = TextIO.openAppend name in
-    TextIO.output (outstream, txt);
-    TextIO.closeOut outstream
-  end;
-
-fun copy infile outfile =
-  if not (exists infile) then error ("File not found: " ^ quote infile)
-  else write outfile (read infile);
-
-val source = Source.of_string o read;
-
-
-end;