# HG changeset patch
# User wenzelm
# Date 897667721 -7200
# Node ID 95f6daba7a9d19d5631c43c24dbf024d81568734
# Parent  8e43dab90429d0a252e2a4995d52f5da23f0279a
added use_text;

diff -r 8e43dab90429 -r 95f6daba7a9d src/Pure/Thy/use.ML
--- a/src/Pure/Thy/use.ML	Fri Jun 12 17:07:33 1998 +0200
+++ b/src/Pure/Thy/use.ML	Fri Jun 12 18:08:41 1998 +0200
@@ -9,6 +9,7 @@
 
 signature USE =
 sig
+  val use_text: string -> string -> unit
   val use: string -> unit
   val exit_use: string -> unit
   val time_use: string -> unit
@@ -18,6 +19,22 @@
 structure Use: USE =
 struct
 
+
+(* use_text *)
+
+val use_orig = use;
+
+fun use_text name txt =
+  let
+    val tmp_name = File.tmp_name ("." ^ Path.base_name name);
+    val _ = File.write tmp_name txt;
+    val rm = OS.FileSys.remove;
+  in
+    use_orig tmp_name handle exn => (rm tmp_name; raise exn);
+    rm tmp_name
+  end;
+
+
 (* generate suffix *)
 
 fun append_suffix name =
@@ -31,8 +48,6 @@
 
 (* input filtering *)
 
-val use_orig = use;
-
 val use_filter =
   if not needs_filtered_use then use_orig
   else
@@ -42,15 +57,7 @@
         val txt_out = Symbol.input txt;
       in
         if txt = txt_out then use_orig name
-        else
-          let
-            val tmp_name = File.tmp_name ("." ^ Path.base_name name);
-            val _ = File.write tmp_name txt_out;
-            val rm = OS.FileSys.remove;
-          in
-            use_orig tmp_name handle exn => (rm tmp_name; raise exn);
-            rm tmp_name
-          end
+        else use_text name txt_out
       end;