# HG changeset patch
# User wenzelm
# Date 918058835 -3600
# Node ID aca4aca5a040dc56346fa22059484d99414a888d
# Parent  9b1be867e21a0b5a18a8887df61c3a54df1e2825
moved to General/use.ML;

diff -r 9b1be867e21a -r aca4aca5a040 src/Pure/Thy/use.ML
--- a/src/Pure/Thy/use.ML	Wed Feb 03 17:20:09 1999 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(*  Title:      Pure/Thy/use.ML
-    ID:         $Id$
-    Author:     David von Oheimb and Markus Wenzel, TU Muenchen
-
-Redefine 'use' command in order to support path variable expansion,
-automatic suffix generation, and symbolic input filtering (if
-required).
-*)
-
-signature USE =
-sig
-  val use: string -> unit
-  val exit_use: string -> unit
-  val time_use: string -> unit
-  val cd: string -> unit
-end;
-
-structure Use: USE =
-struct
-
-(* generate suffix *)
-
-fun append_suffix name =
-  let
-    fun try [] = error ("File not found: " ^ quote name)
-      | try (sfx :: sfxs) =
-          if File.exists (name ^ sfx) then name ^ sfx
-          else try sfxs;
-  in try ["", ".ML", ".sml"] end;
-
-
-(* input filtering *)
-
-val use_orig = use;
-
-val use_filter =
-  if not needs_filtered_use then use_orig
-  else
-    fn name =>
-      let
-        val txt = File.read name;
-        val txt_out = Symbol.input txt;
-      in
-        if txt = txt_out then use_orig name
-        else
-          let
-            val tmp_name = File.tmp_name ("." ^ Path.base_name name);
-            val _ = File.write tmp_name txt_out;
-            val rm = OS.FileSys.remove;
-          in
-            use_orig tmp_name handle exn => (rm tmp_name; raise exn);
-            rm tmp_name
-          end
-      end;
-
-
-(* use commands *)
-
-val use = use_filter o append_suffix o Path.expand getenv;
-
-(*use the file, but exit with error code if errors found*)
-fun exit_use name = use name handle _ => exit 1;
-
-(*timed "use" function, printing filenames*)
-fun time_use name = timeit (fn () =>
-  (writeln ("\n**** Starting " ^ name ^ " ****"); use name;
-   writeln ("\n**** Finished " ^ name ^ " ****")));
-
-
-(* redefine cd *)
-
-val cd = cd o Path.expand getenv;
-
-
-end;