--- 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;