--- a/src/Pure/Thy/use.ML Fri Jun 12 18:08:41 1998 +0200
+++ b/src/Pure/Thy/use.ML Sat Jun 13 18:25:39 1998 +0200
@@ -9,7 +9,6 @@
signature USE =
sig
- val use_text: string -> string -> unit
val use: string -> unit
val exit_use: string -> unit
val time_use: string -> unit
@@ -19,22 +18,6 @@
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 =
@@ -48,6 +31,8 @@
(* input filtering *)
+val use_orig = use;
+
val use_filter =
if not needs_filtered_use then use_orig
else
@@ -57,7 +42,15 @@
val txt_out = Symbol.input txt;
in
if txt = txt_out then use_orig name
- else use_text name txt_out
+ 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
end;