# HG changeset patch
# User wenzelm
# Date 850726968 -3600
# Node ID e1b946f9c8bec2817331b9546d9d2cc0900f2f86
# Parent  edcc26b1461dfb00ce60d90086aed5f9d396062e
symbol_input.ML: Defines 'use' command with symbol input filtering.

diff -r edcc26b1461d -r e1b946f9c8be src/Pure/Thy/symbol_input.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/symbol_input.ML	Mon Dec 16 10:02:48 1996 +0100
@@ -0,0 +1,53 @@
+(*  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 file_exists name = file_info name <> "";
+
+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 infile = TextIO.openIn name;
+        val txt = TextIO.inputAll infile;
+        val _ = TextIO.closeIn infile;
+
+        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 outfile = TextIO.openOut tmp_name;
+            val _ = TextIO.output (outfile, txt_out);
+            val _ = TextIO.closeOut outfile;
+
+            val rm = OS.FileSys.remove;
+          in
+            use tmp_name handle exn => (rm tmp_name; raise exn);
+            rm tmp_name
+          end
+      end;
+
+end;