1.1 --- a/src/Pure/ML-Systems/mlworks.ML Mon Jun 15 11:05:25 1998 +0200
1.2 +++ b/src/Pure/ML-Systems/mlworks.ML Mon Jun 15 11:06:00 1998 +0200
1.3 @@ -66,14 +66,15 @@
1.4 (* ML command execution *)
1.5
1.6 (*Can one redirect 'use' directly to an instream?*)
1.7 -fun use_strings strs =
1.8 +fun use_text txt =
1.9 let
1.10 val tmp_name = OS.FileSys.tmpName ();
1.11 val tmp_file = TextIO.openOut tmp_name;
1.12 - in app (fn s => TextIO.output (tmp_file, s)) strs;
1.13 - TextIO.closeOut tmp_file;
1.14 - use tmp_name;
1.15 - OS.FileSys.remove tmp_name
1.16 + in
1.17 + TextIO.output (tmp_file, txt);
1.18 + TextIO.closeOut tmp_file;
1.19 + use tmp_name;
1.20 + OS.FileSys.remove tmp_name
1.21 end;
1.22
1.23
2.1 --- a/src/Pure/ML-Systems/polyml.ML Mon Jun 15 11:05:25 1998 +0200
2.2 +++ b/src/Pure/ML-Systems/polyml.ML Mon Jun 15 11:06:00 1998 +0200
2.3 @@ -41,22 +41,18 @@
2.4
2.5 (* ML command execution -- 'eval' *)
2.6
2.7 -val use_strings =
2.8 +fun use_text txt =
2.9 let
2.10 - fun exec line =
2.11 - let
2.12 - val is_first = ref true;
2.13 -
2.14 - fun get_line () =
2.15 - if ! is_first then (is_first := false; line)
2.16 - else raise Io "use_strings: buffer exhausted";
2.17 - in
2.18 - PolyML.compiler (get_line, print) ()
2.19 - end;
2.20 -
2.21 - fun execs [] = ()
2.22 - | execs (line :: lines) = (exec line; execs lines);
2.23 - in execs end;
2.24 + val buffer = ref (explode txt);
2.25 + fun get () =
2.26 + (case ! buffer of
2.27 + [] => ""
2.28 + | c :: cs => (buffer := cs; c));
2.29 + fun exec () =
2.30 + (case ! buffer of
2.31 + [] => ()
2.32 + | _ => (PolyML.compiler (get, print) (); exec ()));
2.33 + in exec () end;
2.34
2.35
2.36
3.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML Mon Jun 15 11:05:25 1998 +0200
3.2 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML Mon Jun 15 11:06:00 1998 +0200
3.3 @@ -81,8 +81,7 @@
3.4
3.5 (* ML command execution *)
3.6
3.7 -fun use_strings commands =
3.8 - System.Compile.use_stream (open_string (implode commands));
3.9 +val use_text = System.Compile.use_stream o open_string;
3.10
3.11
3.12
4.1 --- a/src/Pure/ML-Systems/smlnj.ML Mon Jun 15 11:05:25 1998 +0200
4.2 +++ b/src/Pure/ML-Systems/smlnj.ML Mon Jun 15 11:06:00 1998 +0200
4.3 @@ -82,7 +82,7 @@
4.4
4.5 (* ML command execution *)
4.6
4.7 -val use_strings = Compiler.Interact.useStream o TextIO.openString o implode;
4.8 +val use_text = Compiler.Interact.useStream o TextIO.openString;
4.9
4.10
4.11
5.1 --- a/src/Pure/Thy/thm_database.ML Mon Jun 15 11:05:25 1998 +0200
5.2 +++ b/src/Pure/Thy/thm_database.ML Mon Jun 15 11:06:00 1998 +0200
5.3 @@ -52,7 +52,7 @@
5.4 let val thm' = store_thm (name, thm) in
5.5 if is_ml_identifier name then
5.6 (qed_thm := Some thm';
5.7 - use_strings ["val " ^ name ^ " = the (! ThmDatabase.qed_thm);"])
5.8 + use_text ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
5.9 else warning ("Cannot bind thm " ^ quote name ^ " as ML value")
5.10 end;
5.11
6.1 --- a/src/Pure/Thy/thy_read.ML Mon Jun 15 11:05:25 1998 +0200
6.2 +++ b/src/Pure/Thy/thy_read.ML Mon Jun 15 11:06:00 1998 +0200
6.3 @@ -267,7 +267,7 @@
6.4 Use.use ml_file);
6.5
6.6 (*Store theory again because it could have been redefined*)
6.7 - use_strings ["val _ = store_theory " ^ tname ^ ".thy;"];
6.8 + use_text ("val _ = store_theory " ^ tname ^ ".thy;");
6.9
6.10 (*Add theory to list of all loaded theories (for index.html)
6.11 and add it to its parents' sub-charts*)