# HG changeset patch
# User wenzelm
# Date 918148329 -3600
# Node ID ef938c8ef653a85b8ce8c5aa8d34eeda7285aae5
# Parent  5a29b53eca4595445ac28420fb9fb57b6d5893c4
removed General/use.ML;

diff -r 5a29b53eca45 -r ef938c8ef653 src/Pure/General/use.ML
--- a/src/Pure/General/use.ML	Wed Feb 03 20:56:29 1999 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(*  Title:      Pure/General/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
-by the underlying ML system).
-*)
-
-signature BASIC_USE =
-sig
-  val use: string -> unit
-  val exit_use: string -> unit
-  val time_use: string -> unit
-  val cd: string -> unit
-end;
-
-signature USE =
-sig
-  include BASIC_USE
-  val use_path: Path.T -> unit
-end;
-
-structure Use: USE =
-struct
-
-(* generate suffix *)   (* FIXME elim (cf. Thy/thy_load) (!?) *)
-
-fun append_suffix path =
-  let
-    fun try [] = error ("File not found: " ^ quote (Path.pack path))
-      | try (sfx :: sfxs) =
-          let val xpath = Path.ext sfx path
-          in if File.exists xpath then xpath else try sfxs end;
-  in try ["", "ML", "sml"] end;
-
-
-(* input filtering *)
-
-val use_path =
-  if not needs_filtered_use then File.use
-  else
-    fn path =>
-      let
-        val txt = File.read path;
-        val txt_out = Symbol.input txt;
-      in
-        if txt = txt_out then File.use path
-        else
-          let val tmp_path = File.tmp_path path in
-            File.write tmp_path txt_out;
-            File.use tmp_path handle exn => (File.rm tmp_path; raise exn);
-            File.rm tmp_path
-          end
-      end;
-
-
-(* use commands *)
-
-val use = use_path o append_suffix o Path.unpack;
-
-(*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 ^ " ****")));
-
-
-(* cd *)
-
-val cd = File.cd o Path.unpack;
-
-
-end;
-
-structure BasicUse: BASIC_USE = Use;    (*opened later*)
diff -r 5a29b53eca45 -r ef938c8ef653 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Feb 03 20:56:29 1999 +0100
+++ b/src/Pure/IsaMakefile	Thu Feb 04 18:12:09 1999 +0100
@@ -27,7 +27,7 @@
   General/history.ML General/name_space.ML General/object.ML \
   General/path.ML General/position.ML General/pretty.ML \
   General/scan.ML General/seq.ML General/source.ML General/symbol.ML \
-  General/table.ML General/use.ML Isar/ROOT.ML Isar/args.ML \
+  General/table.ML Isar/ROOT.ML Isar/args.ML \
   Isar/attrib.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
   Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
   Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \