1.1 --- a/src/Pure/ML-Systems/MLWorks.ML Wed Aug 06 14:35:52 1997 +0200
1.2 +++ b/src/Pure/ML-Systems/MLWorks.ML Wed Aug 06 14:42:44 1997 +0200
1.3 @@ -84,7 +84,7 @@
1.4 val tmpName = OS.FileSys.tmpName();
1.5
1.6 (*Can one redirect 'use' directly to an instream?*)
1.7 -fun use_string slist =
1.8 +fun use_strings slist =
1.9 let val tmpFile = TextIO.openOut tmpName
1.10 in app (fn s => TextIO.output (tmpFile, s)) slist;
1.11 TextIO.closeOut tmpFile;
2.1 --- a/src/Pure/ML-Systems/polyml.ML Wed Aug 06 14:35:52 1997 +0200
2.2 +++ b/src/Pure/ML-Systems/polyml.ML Wed Aug 06 14:42:44 1997 +0200
2.3 @@ -42,7 +42,7 @@
2.4
2.5 (* ML command execution -- 'eval' *)
2.6
2.7 -val use_string =
2.8 +val use_strings =
2.9 let
2.10 fun exec line =
2.11 let
2.12 @@ -50,7 +50,7 @@
2.13
2.14 fun get_line () =
2.15 if ! is_first then (is_first := false; line)
2.16 - else raise Io "use_string: buffer exhausted";
2.17 + else raise Io "use_strings: buffer exhausted";
2.18 in
2.19 PolyML.compiler (get_line, print) ()
2.20 end;
3.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML Wed Aug 06 14:35:52 1997 +0200
3.2 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML Wed Aug 06 14:42:44 1997 +0200
3.3 @@ -30,34 +30,29 @@
3.4 (* timing *)
3.5
3.6 local
3.7 -
3.8 -(*print microseconds, suppressing trailing zeroes*)
3.9 -fun umakestring 0 = ""
3.10 - | umakestring n =
3.11 - chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
3.12 -
3.13 + (*print microseconds, suppressing trailing zeroes*)
3.14 + fun umakestring 0 = ""
3.15 + | umakestring n =
3.16 + chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
3.17 in
3.18 -
3.19 -(*a conditional timing function: applies f to () and, if the flag is true,
3.20 - prints its runtime*)
3.21 -
3.22 -fun cond_timeit flag f =
3.23 - if flag then
3.24 - let fun string_of_time (System.Timer.TIME {sec, usec}) =
3.25 - makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
3.26 - open System.Timer;
3.27 - val start = start_timer()
3.28 - val result = f();
3.29 - val nongc = check_timer(start)
3.30 - and gc = check_timer_gc(start);
3.31 - val both = add_time(nongc, gc)
3.32 - in print("Non GC " ^ string_of_time nongc ^
3.33 - " GC " ^ string_of_time gc ^
3.34 - " both "^ string_of_time both ^ " secs\n");
3.35 - result
3.36 - end
3.37 - else f();
3.38 -
3.39 + (*a conditional timing function: applies f to () and, if the flag is true,
3.40 + prints its runtime*)
3.41 + fun cond_timeit flag f =
3.42 + if flag then
3.43 + let fun string_of_time (System.Timer.TIME {sec, usec}) =
3.44 + makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
3.45 + open System.Timer;
3.46 + val start = start_timer()
3.47 + val result = f();
3.48 + val nongc = check_timer(start)
3.49 + and gc = check_timer_gc(start);
3.50 + val both = add_time(nongc, gc)
3.51 + in print("Non GC " ^ string_of_time nongc ^
3.52 + " GC " ^ string_of_time gc ^
3.53 + " both "^ string_of_time both ^ " secs\n");
3.54 + result
3.55 + end
3.56 + else f();
3.57 end;
3.58
3.59
3.60 @@ -81,7 +76,7 @@
3.61
3.62 (* ML command execution *)
3.63
3.64 -fun use_string commands =
3.65 +fun use_strings commands =
3.66 System.Compile.use_stream (open_string (implode commands));
3.67
3.68
4.1 --- a/src/Pure/ML-Systems/smlnj-1.09.ML Wed Aug 06 14:35:52 1997 +0200
4.2 +++ b/src/Pure/ML-Systems/smlnj-1.09.ML Wed Aug 06 14:42:44 1997 +0200
4.3 @@ -80,7 +80,7 @@
4.4
4.5 (* ML command execution *)
4.6
4.7 -val use_string = Compiler.Interact.useStream o TextIO.openString o implode;
4.8 +val use_strings = Compiler.Interact.useStream o TextIO.openString o implode;
4.9
4.10
4.11
5.1 --- a/src/Pure/Thy/thm_database.ML Wed Aug 06 14:35:52 1997 +0200
5.2 +++ b/src/Pure/Thy/thm_database.ML Wed Aug 06 14:42:44 1997 +0200
5.3 @@ -307,22 +307,22 @@
5.4
5.5 fun bind_thm (name, thm) =
5.6 (qed_thm := store_thm (name, (standard thm));
5.7 - use_string ["val " ^ name ^ " = !qed_thm;"]);
5.8 + use_strings ["val " ^ name ^ " = !qed_thm;"]);
5.9
5.10
5.11 fun qed name =
5.12 (qed_thm := store_thm (name, result ());
5.13 - use_string ["val " ^ name ^ " = !qed_thm;"]);
5.14 + use_strings ["val " ^ name ^ " = !qed_thm;"]);
5.15
5.16
5.17 fun qed_goal name thy agoal tacsf =
5.18 (qed_thm := store_thm (name, prove_goal thy agoal tacsf);
5.19 - use_string ["val " ^ name ^ " = !qed_thm;"]);
5.20 + use_strings ["val " ^ name ^ " = !qed_thm;"]);
5.21
5.22
5.23 fun qed_goalw name thy rths agoal tacsf =
5.24 (qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf);
5.25 - use_string ["val " ^ name ^ " = !qed_thm;"]);
5.26 + use_strings ["val " ^ name ^ " = !qed_thm;"]);
5.27
5.28
5.29 (** Retrieve theorems **)
6.1 --- a/src/Pure/Thy/thy_read.ML Wed Aug 06 14:35:52 1997 +0200
6.2 +++ b/src/Pure/Thy/thy_read.ML Wed Aug 06 14:42:44 1997 +0200
6.3 @@ -314,7 +314,7 @@
6.4 save_data false;
6.5
6.6 (*Store theory again because it could have been redefined*)
6.7 - use_string
6.8 + use_strings
6.9 ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
6.10
6.11 (*Add theory to list of all loaded theories (for index.html)