--- a/src/Pure/Thy/symbol_input.ML Wed Nov 12 16:25:45 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(* Title: Pure/Thy/symbol_input.ML
- ID: $Id$
- Author: David von Oheimb and Markus Wenzel, TU Muenchen
-
-Defines 'use' command with symbol input filtering.
-*)
-
-signature SYMBOL_INPUT =
-sig
- val use: string -> unit
-end;
-
-structure SymbolInput: SYMBOL_INPUT =
-struct
-
-fun fix_name name =
- if file_exists name then name
- else if file_exists (name ^ ".ML") then name ^ ".ML"
- else if file_exists (name ^ ".sml") then name ^ ".sml"
- else error ("File not found: " ^ quote name);
-
-
-val use =
- if not needs_filtered_use then use
- else
- fn raw_name =>
- let
- val name = fix_name raw_name;
- val txt = read_file name;
- val txt_out = implode (SymbolFont.write_charnames' (explode txt));
- in
- if txt = txt_out then use name
- else
- let
- val tmp_name = "/tmp/" ^ base_name name; (* FIXME unique prefix (!?) *)
- val _ = write_file tmp_name txt_out;
- val rm = OS.FileSys.remove;
- in
- use tmp_name handle exn => (rm tmp_name; raise exn);
- rm tmp_name
- end
- end;
-
-end;