# HG changeset patch
# User wenzelm
# Date 918148480 -3600
# Node ID f453bd781dfd1008e99885d9c4531ebcb2a5fdd5
# Parent  0c08846be6f3d4f921d5549c78c0a9901e4c8d8a
added 'use';

diff -r 0c08846be6f3 -r f453bd781dfd src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Feb 04 18:14:27 1999 +0100
+++ b/src/Pure/General/symbol.ML	Thu Feb 04 18:14:40 1999 +0100
@@ -29,6 +29,7 @@
   val output: string -> string
   val source: bool -> (string, 'a) Source.source ->
     (symbol, (string, 'a) Source.source) Source.source
+  val use: Path.T -> unit
 end;
 
 structure Symbol: SYMBOL =
@@ -269,10 +270,29 @@
 		in (implode o map chr o sym_explode) s end;
 
 
+(* version of 'use' with input filtering *)
+
+val use =
+  if not needs_filtered_use then File.use
+  else
+    fn path =>
+      let
+        val txt = File.read path;
+        val txt_out = 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;
+
+
 (*final declarations of this structure!*)
 val explode = sym_explode;
 val length = sym_length;
 val size = sym_size;
 
-
 end;