# HG changeset patch
# User wenzelm
# Date 879348365 -3600
# Node ID 3cc85acd9ba85e1f66827a3dab353a8f37aa5d97
# Parent  276e53e5ceca55449e1bfb20892f10b834e1d626
renamed to use.ML;

diff -r 276e53e5ceca -r 3cc85acd9ba8 src/Pure/Thy/symbol_input.ML
--- 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;