removed General/use.ML;
authorwenzelm
Thu Feb 04 18:12:09 1999 +0100 (1999-02-04)
changeset 6221ef938c8ef653
parent 6220 5a29b53eca45
child 6222 2b24cf477313
removed General/use.ML;
src/Pure/General/use.ML
src/Pure/IsaMakefile
     1.1 --- a/src/Pure/General/use.ML	Wed Feb 03 20:56:29 1999 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,78 +0,0 @@
     1.4 -(*  Title:      Pure/General/use.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     David von Oheimb and Markus Wenzel, TU Muenchen
     1.7 -
     1.8 -Redefine 'use' command in order to support path variable expansion,
     1.9 -automatic suffix generation, and symbolic input filtering (if required
    1.10 -by the underlying ML system).
    1.11 -*)
    1.12 -
    1.13 -signature BASIC_USE =
    1.14 -sig
    1.15 -  val use: string -> unit
    1.16 -  val exit_use: string -> unit
    1.17 -  val time_use: string -> unit
    1.18 -  val cd: string -> unit
    1.19 -end;
    1.20 -
    1.21 -signature USE =
    1.22 -sig
    1.23 -  include BASIC_USE
    1.24 -  val use_path: Path.T -> unit
    1.25 -end;
    1.26 -
    1.27 -structure Use: USE =
    1.28 -struct
    1.29 -
    1.30 -(* generate suffix *)   (* FIXME elim (cf. Thy/thy_load) (!?) *)
    1.31 -
    1.32 -fun append_suffix path =
    1.33 -  let
    1.34 -    fun try [] = error ("File not found: " ^ quote (Path.pack path))
    1.35 -      | try (sfx :: sfxs) =
    1.36 -          let val xpath = Path.ext sfx path
    1.37 -          in if File.exists xpath then xpath else try sfxs end;
    1.38 -  in try ["", "ML", "sml"] end;
    1.39 -
    1.40 -
    1.41 -(* input filtering *)
    1.42 -
    1.43 -val use_path =
    1.44 -  if not needs_filtered_use then File.use
    1.45 -  else
    1.46 -    fn path =>
    1.47 -      let
    1.48 -        val txt = File.read path;
    1.49 -        val txt_out = Symbol.input txt;
    1.50 -      in
    1.51 -        if txt = txt_out then File.use path
    1.52 -        else
    1.53 -          let val tmp_path = File.tmp_path path in
    1.54 -            File.write tmp_path txt_out;
    1.55 -            File.use tmp_path handle exn => (File.rm tmp_path; raise exn);
    1.56 -            File.rm tmp_path
    1.57 -          end
    1.58 -      end;
    1.59 -
    1.60 -
    1.61 -(* use commands *)
    1.62 -
    1.63 -val use = use_path o append_suffix o Path.unpack;
    1.64 -
    1.65 -(*use the file, but exit with error code if errors found*)
    1.66 -fun exit_use name = use name handle _ => exit 1;
    1.67 -
    1.68 -(*timed "use" function, printing filenames*)
    1.69 -fun time_use name = timeit (fn () =>
    1.70 -  (writeln ("\n**** Starting " ^ name ^ " ****"); use name;
    1.71 -   writeln ("\n**** Finished " ^ name ^ " ****")));
    1.72 -
    1.73 -
    1.74 -(* cd *)
    1.75 -
    1.76 -val cd = File.cd o Path.unpack;
    1.77 -
    1.78 -
    1.79 -end;
    1.80 -
    1.81 -structure BasicUse: BASIC_USE = Use;    (*opened later*)
     2.1 --- a/src/Pure/IsaMakefile	Wed Feb 03 20:56:29 1999 +0100
     2.2 +++ b/src/Pure/IsaMakefile	Thu Feb 04 18:12:09 1999 +0100
     2.3 @@ -27,7 +27,7 @@
     2.4    General/history.ML General/name_space.ML General/object.ML \
     2.5    General/path.ML General/position.ML General/pretty.ML \
     2.6    General/scan.ML General/seq.ML General/source.ML General/symbol.ML \
     2.7 -  General/table.ML General/use.ML Isar/ROOT.ML Isar/args.ML \
     2.8 +  General/table.ML Isar/ROOT.ML Isar/args.ML \
     2.9    Isar/attrib.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
    2.10    Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
    2.11    Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \